Theorem 3ad2ant1 800

Description: Deduction adding conjuncts to an antecedent.

Hypothesis

Ref	Expression
3ad2ant.1	|- (ph -> ch)

Assertion

Ref	Expression
3ad2ant1	|- ((ph /\ ps /\ th) -> ch)

Proof of Theorem 3ad2ant1

Step	Hyp	Ref	Expression
1		3ad2ant.1	. . 3 |- (ph -> ch)
2	1	adantr 389	. 2 |- ((ph /\ th) -> ch)
3	2	3adant2 798	1 |- ((ph /\ ps /\ th) -> ch)

Syntax hints:   -> wi 3   /\ w3a 775

This theorem is referenced by:  sbciegft 1959  itlso 2863  reuuniss 2889  oneo 4212  fodomr 4483  alephval3 4903  ltasr 5209  cnegextlem1 5345  divdivmult 5795  ltmulgt11t 5846  lt2mul2divt 5872  lediv2t 5891  ledivp1 5906  ltdivp1 5907  suprleub 6059  supxrun 6085  gtndivt 6193  lbicc2t 6404  icoshftf1olem 6410  eluzp1p1t 6435  infmssuzle 6465  eluzfz1t 6487  seqzvalt 6540  seqzval2t 6553  seqzcl 6558  expwordit 6603  expword2it 6605  expubndt 6608  sqlecant 6641  bernneq2 6653  expnlbndt 6655  mulretOLD 6777  fsum1p 7019  fsumshft 7031  serz1p 7052  serzmulc1 7057  iserzgt0 7211  isummulc1 7212  ivthlem6 7286  ivthlem7 7287  sin02gt0 7478  tgtop11t 7634  tgsst 7636  elcls3 7711  neiint 7719  neips 7727  opnneissb 7728  opnssneib 7729  islp2 7747  iscnp2 7761  cnpco 7769  cnconst 7780  bl2in 7843  metcnpf 7883  metcnp 7887  metidcn 7900  metdnsconst 7901  cncfmet 7905  tgioolem 7914  caussi 7954  iscms2lem4 7992  grpdivval 8082  imsdval 8317  nvelbl 8325  nvcnpf 8328  nvcni 8329  nvcni2 8330  nvlmle 8333  ipval 8353  lno0 8417  nvcnpi3 8422  nvcnpi4 8423  nmoubi 8435  nmobndi 8438  isblo3i 8461  phpar2 8482  phpar 8483  spwval2 8653  pilem1 8671  sinq12gt0t 8708  sincosq1eq 8709  efif1lem1 8730  efif1lem2 8731  his52t 8954  bcs2t 9049  spansncol 9491  pjspansnt 9500  nmoplbt 9831  nmopubt 9832  unopt 9839  hmopt 9846  nmfnlbt 9848  nmfnleubt 9849  lnopmult 9891  nmcopexlem5 9955  nmcfnexlem5 9984  leopmult 10067  hstelt 10142  ghomid 10394  ghomf1olem 10396  truni1 10499  homeofval 10516  hmphsyma 10528  homcard 10539  hmeobc 10542  fipfil2 10564  fipfil2OLD 10565  neifil 10568  filintf 10569  fgsb 10570  fgsbOLD 10571  cnfilca 10583  cnfilcaOLD 10584  rcfpfillem6 10595  rcfpfillem6OLD 10596  mslb1 10629  2wsms 10630  1cat 10692  cmpmorp 10712  icmpmon 10744  idfisf 10760

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 777

Copyright terms: Public domain