Theorem 3ad2ant2 1043

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 1039	1 |- ( ( ps /\ ph /\ th ) -> ch )

Syntax hints:   -> wi 4   /\ w3a 1002

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 1004

This theorem is referenced by:  simp2l  1047  simp2r  1048  simp21  1054  simp22  1055  simp23  1056  simp2ll  1088  simp2lr  1089  simp2rl  1090  simp2rr  1091  simp2l1  1120  simp2l2  1121  simp2l3  1122  simp2r1  1123  simp2r2  1124  simp2r3  1125  simp21l  1138  simp21r  1139  simp22l  1140  simp22r  1141  simp23l  1142  simp23r  1143  simp211  1159  simp212  1160  simp213  1161  simp221  1162  simp222  1163  simp223  1164  simp231  1165  simp232  1166  simp233  1167  3anim123i  1208  3jaao  1342  ceqsalt  2826  vtoclgft  2851  vtoclegft  2875  ifbothdc  3637  ifnebibdc  3648  frirrg  4441  elirr  4633  en2lp  4646  reg3exmidlemwe  4671  sotri3  5127  funtpg  5372  fnprg  5376  fntpg  5377  funimaexglem  5404  fnco  5431  fvun1  5702  oprssov  6153  caovimo  6205  rdgivallem  6533  fnsnsplitdc  6659  funresdfunsndc  6660  f1dom2g  6915  mapxpen  7017  ssfidc  7110  sbthlemi4  7138  ordiso2  7213  updjud  7260  difinfsn  7278  mkvprop  7336  endjudisj  7403  distrnqg  7585  distrnq0  7657  prarloclem5  7698  cauappcvgprlemlol  7845  cauappcvgprlemupu  7847  caucvgprlemlol  7868  caucvgprlemupu  7870  caucvgprprlemlol  7896  caucvgprprlemupu  7898  cnegexlem2  8333  apcotr  8765  apadd1  8766  mulext1  8770  div2negap  8893  ltdiv2  9045  nndivtr  9163  difgtsumgt  9527  zdivmul  9548  gtndiv  9553  fzind  9573  eluzuzle  9742  eluzp1p1  9760  peano2uz  9790  qdivcl  9850  irrmul  9854  ledivge1le  9934  xrre2  10029  xaddass  10077  xltadd1  10084  xlt2add  10088  ubioc1  10137  ubicc2  10193  zltaddlt1le  10215  uzsubsubfz  10255  elfz1b  10298  fzp1nel  10312  fz0fzdiffz0  10338  difelfzle  10342  elfzo0  10394  elfzonlteqm1  10428  fzonn0p1p1  10431  fzosplitprm1  10452  fzoshftral  10456  subfzo0  10460  ceiqle  10547  modqval  10558  modqvalr  10559  flqpmodeq  10561  modq0  10563  mulqmod0  10564  negqmod0  10565  modqge0  10566  modqlt  10567  modqelico  10568  modqdiffl  10569  modqmulnn  10576  modqvalp1  10577  modqmuladdnn0  10602  qnegmod  10603  addmodid  10606  q2submod  10619  modifeq2int  10620  modfzo0difsn  10629  addmodlteq  10632  mulsubdivbinom2ap  10945  omgadd  11036  hashun  11039  ccatass  11156  lswccatn0lsw  11159  ccats1val2  11187  swrd00g  11197  swrdval2  11199  swrdlen  11200  swrdfv  11201  swrdfv0  11202  swrdnd  11207  swrdlen2  11210  swrdfv2  11211  swrdsbslen  11214  swrdspsleq  11215  ccatswrd  11218  pfxfv  11232  pfxn0  11236  pfxnd  11237  pfxsuff1eqwrdeq  11247  pfxpfx  11256  ccats1pfxeq  11262  ccatopth2  11265  wrd2ind  11271  pfxccatin12lem3  11280  pfxccat3  11282  swrdccat  11283  pfxccat3a  11286  redivap  11401  imdivap  11408  xrmaxltsup  11785  xrmaxadd  11788  xrlemininf  11798  xrminltinf  11799  climuni  11820  mulcn2  11839  fsumsplitsnun  11946  prodfap0  12072  fprodabs  12143  efsub  12208  cos12dec  12295  dvdsmodexp  12322  summodnegmod  12349  divalglemex  12449  divalg  12451  modremain  12456  ndvdssub  12457  fldivndvdslt  12464  bitsfzo  12482  nndvdslegcd  12502  dfgcd2  12551  mulgcd  12553  mulgcdr  12555  gcddiv  12556  rplpwr  12564  rppwr  12565  qredeq  12634  divgcdcoprmex  12640  cncongr1  12641  cncongr2  12642  pw2dvdslemn  12703  hashgcdlem  12776  modprm0  12793  modprmn0modprm0  12795  pythagtriplem1  12804  pythagtriplem3  12806  pythagtriplem10  12808  pythagtriplem6  12809  pythagtriplem7  12810  pythagtriplem11  12813  pythagtriplem12  12814  pythagtriplem13  12815  pythagtriplem14  12816  pythagtriplem19  12821  pythagtrip  12822  dvdsprmpweqnn  12875  difsqpwdvds  12877  pcfaclem  12888  pcbc  12890  unennn  12984  ptex  13313  imasaddvallemg  13364  fvprif  13392  mgmsscl  13410  insubm  13534  mulginvcom  13700  mulgassr  13713  mulgmodid  13714  quselbasg  13783  ghmnsgima  13821  ringrng  14015  rmodislmodlem  14330  rmodislmod  14331  lssincl  14365  sralmod  14430  rnglidlmmgm  14476  rnglidlmsgrp  14477  rnglidlrng  14478  2idlcpblrng  14503  psrbaglesuppg  14652  ntrin  14814  elnei  14842  restco  14864  cnpnei  14909  cncnp2m  14921  sslm  14937  upxp  14962  blres  15124  metcnp3  15201  tgqioo  15245  dvply1  15455  ptolemy  15514  cxpcom  15628  logbgcd1irr  15657  logbprmirr  15662  lgslem1  15695  lgsneg  15719  lgsdilem  15722  lgsdir  15730  lgssq2  15736  lgsdirnn0  15742  gausslemma2dlem1a  15753  2lgslem1a1  15781  incistruhgr  15906  upgrex  15919  uhgr2edg  16020  iedginwlk  16103  uspgr2wlkeq2  16112  umgrclwwlkge2  16145  clwwlkext2edg  16164  clwwlknccat  16165  umgr2cwwk2dif  16166  umgr2cwwkdifex  16167