Theorem 3ad2ant2 1021

Description: Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)

Hypothesis

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

Assertion

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

Proof of Theorem 3ad2ant2

Step	Hyp	Ref	Expression
1		3ad2ant.1	. . 3 |- ( ph -> ch )
2	1	adantr 276	. 2 |- ( ( ph /\ th ) -> ch )
3	2	3adant1 1017	1 |- ( ( ps /\ ph /\ th ) -> ch )

Syntax hints:   -> wi 4   /\ w3a 980

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  simp2l  1025  simp2r  1026  simp21  1032  simp22  1033  simp23  1034  simp2ll  1066  simp2lr  1067  simp2rl  1068  simp2rr  1069  simp2l1  1098  simp2l2  1099  simp2l3  1100  simp2r1  1101  simp2r2  1102  simp2r3  1103  simp21l  1116  simp21r  1117  simp22l  1118  simp22r  1119  simp23l  1120  simp23r  1121  simp211  1137  simp212  1138  simp213  1139  simp221  1140  simp222  1141  simp223  1142  simp231  1143  simp232  1144  simp233  1145  3anim123i  1186  3jaao  1319  ceqsalt  2789  vtoclgft  2814  vtoclegft  2836  ifbothdc  3594  ifnebibdc  3604  frirrg  4385  elirr  4577  en2lp  4590  reg3exmidlemwe  4615  sotri3  5068  funtpg  5309  fnprg  5313  fntpg  5314  funimaexglem  5341  fnco  5366  fvun1  5627  oprssov  6065  caovimo  6117  rdgivallem  6439  fnsnsplitdc  6563  funresdfunsndc  6564  f1dom2g  6815  mapxpen  6909  ssfidc  6998  sbthlemi4  7026  ordiso2  7101  updjud  7148  difinfsn  7166  mkvprop  7224  endjudisj  7277  distrnqg  7454  distrnq0  7526  prarloclem5  7567  cauappcvgprlemlol  7714  cauappcvgprlemupu  7716  caucvgprlemlol  7737  caucvgprlemupu  7739  caucvgprprlemlol  7765  caucvgprprlemupu  7767  cnegexlem2  8202  apcotr  8634  apadd1  8635  mulext1  8639  div2negap  8762  ltdiv2  8914  nndivtr  9032  difgtsumgt  9395  zdivmul  9416  gtndiv  9421  fzind  9441  eluzuzle  9609  eluzp1p1  9627  peano2uz  9657  qdivcl  9717  irrmul  9721  ledivge1le  9801  xrre2  9896  xaddass  9944  xltadd1  9951  xlt2add  9955  ubioc1  10004  ubicc2  10060  zltaddlt1le  10082  uzsubsubfz  10122  elfz1b  10165  fzp1nel  10179  fz0fzdiffz0  10205  difelfzle  10209  elfzo0  10258  elfzonlteqm1  10286  fzonn0p1p1  10289  fzosplitprm1  10310  fzoshftral  10314  subfzo0  10318  ceiqle  10405  modqval  10416  modqvalr  10417  flqpmodeq  10419  modq0  10421  mulqmod0  10422  negqmod0  10423  modqge0  10424  modqlt  10425  modqelico  10426  modqdiffl  10427  modqmulnn  10434  modqvalp1  10435  modqmuladdnn0  10460  qnegmod  10461  addmodid  10464  q2submod  10477  modifeq2int  10478  modfzo0difsn  10487  addmodlteq  10490  mulsubdivbinom2ap  10803  omgadd  10894  hashun  10897  redivap  11039  imdivap  11046  xrmaxltsup  11423  xrmaxadd  11426  xrlemininf  11436  xrminltinf  11437  climuni  11458  mulcn2  11477  fsumsplitsnun  11584  prodfap0  11710  fprodabs  11781  efsub  11846  cos12dec  11933  dvdsmodexp  11960  summodnegmod  11987  divalglemex  12087  divalg  12089  modremain  12094  ndvdssub  12095  fldivndvdslt  12102  bitsfzo  12119  nndvdslegcd  12132  dfgcd2  12181  mulgcd  12183  mulgcdr  12185  gcddiv  12186  rplpwr  12194  rppwr  12195  qredeq  12264  divgcdcoprmex  12270  cncongr1  12271  cncongr2  12272  pw2dvdslemn  12333  hashgcdlem  12406  modprm0  12423  modprmn0modprm0  12425  pythagtriplem1  12434  pythagtriplem3  12436  pythagtriplem10  12438  pythagtriplem6  12439  pythagtriplem7  12440  pythagtriplem11  12443  pythagtriplem12  12444  pythagtriplem13  12445  pythagtriplem14  12446  pythagtriplem19  12451  pythagtrip  12452  dvdsprmpweqnn  12505  difsqpwdvds  12507  pcfaclem  12518  pcbc  12520  unennn  12614  ptex  12935  imasaddvallemg  12958  fvprif  12986  mgmsscl  13004  insubm  13117  mulginvcom  13277  mulgassr  13290  mulgmodid  13291  quselbasg  13360  ghmnsgima  13398  ringrng  13592  rmodislmodlem  13906  rmodislmod  13907  lssincl  13941  sralmod  14006  rnglidlmmgm  14052  rnglidlmsgrp  14053  rnglidlrng  14054  2idlcpblrng  14079  psrbaglesuppg  14226  ntrin  14360  elnei  14388  restco  14410  cnpnei  14455  cncnp2m  14467  sslm  14483  upxp  14508  blres  14670  metcnp3  14747  tgqioo  14791  dvply1  15001  ptolemy  15060  cxpcom  15174  logbgcd1irr  15203  logbprmirr  15208  lgslem1  15241  lgsneg  15265  lgsdilem  15268  lgsdir  15276  lgssq2  15282  lgsdirnn0  15288  gausslemma2dlem1a  15299  2lgslem1a1  15327