Theorem 3ad2ant2 1046

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

Syntax hints:   -> wi 4   /\ w3a 1005

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 1007

This theorem is referenced by:  simp2l  1050  simp2r  1051  simp21  1057  simp22  1058  simp23  1059  simp2ll  1091  simp2lr  1092  simp2rl  1093  simp2rr  1094  simp2l1  1123  simp2l2  1124  simp2l3  1125  simp2r1  1126  simp2r2  1127  simp2r3  1128  simp21l  1141  simp21r  1142  simp22l  1143  simp22r  1144  simp23l  1145  simp23r  1146  simp211  1162  simp212  1163  simp213  1164  simp221  1165  simp222  1166  simp223  1167  simp231  1168  simp232  1169  simp233  1170  3anim123i  1211  3jaao  1345  ceqsalt  2830  vtoclgft  2855  vtoclegft  2879  ifbothdc  3644  ifnebibdc  3655  frirrg  4453  elirr  4645  en2lp  4658  reg3exmidlemwe  4683  sotri3  5142  funtpg  5388  fnprg  5392  fntpg  5393  funimaexglem  5420  fnco  5447  fvun1  5721  oprssov  6174  caovimo  6226  suppsnopdc  6428  funsssuppss  6436  rdgivallem  6590  fnsnsplitdc  6716  funresdfunsndc  6717  f1dom2g  6972  mapxpen  7077  ssfidc  7173  sbthlemi4  7202  ordiso2  7294  updjud  7341  difinfsn  7359  mkvprop  7417  endjudisj  7485  distrnqg  7667  distrnq0  7739  prarloclem5  7780  cauappcvgprlemlol  7927  cauappcvgprlemupu  7929  caucvgprlemlol  7950  caucvgprlemupu  7952  caucvgprprlemlol  7978  caucvgprprlemupu  7980  cnegexlem2  8414  apcotr  8846  apadd1  8847  mulext1  8851  div2negap  8974  ltdiv2  9126  nndivtr  9244  difgtsumgt  9610  zdivmul  9631  gtndiv  9636  fzind  9656  eluzuzle  9825  eluzp1p1  9843  peano2uz  9878  qdivcl  9938  irrmul  9942  ledivge1le  10022  xrre2  10117  xaddass  10165  xltadd1  10172  xlt2add  10176  ubioc1  10225  ubicc2  10281  zltaddlt1le  10304  uzsubsubfz  10344  elfz1b  10387  fzp1nel  10401  fz0fzdiffz0  10427  difelfzle  10431  elfzo0  10483  elfzonlteqm1  10518  fzonn0p1p1  10521  fzosplitprm1  10543  fzoshftral  10547  subfzo0  10551  ceiqle  10638  modqval  10649  modqvalr  10650  flqpmodeq  10652  modq0  10654  mulqmod0  10655  negqmod0  10656  modqge0  10657  modqlt  10658  modqelico  10659  modqdiffl  10660  modqmulnn  10667  modqvalp1  10668  modqmuladdnn0  10693  qnegmod  10694  addmodid  10697  q2submod  10710  modifeq2int  10711  modfzo0difsn  10720  addmodlteq  10723  mulsubdivbinom2ap  11036  omgadd  11128  hashun  11131  ccatass  11251  lswccatn0lsw  11254  ccats1val2  11283  swrd00g  11296  swrdval2  11298  swrdlen  11299  swrdfv  11300  swrdfv0  11301  swrdnd  11306  swrdlen2  11309  swrdfv2  11310  swrdsbslen  11313  swrdspsleq  11314  ccatswrd  11317  pfxfv  11331  pfxn0  11335  pfxnd  11336  pfxsuff1eqwrdeq  11346  pfxpfx  11355  ccats1pfxeq  11361  ccatopth2  11364  wrd2ind  11370  pfxccatin12lem3  11379  pfxccat3  11381  swrdccat  11382  pfxccat3a  11385  redivap  11514  imdivap  11521  xrmaxltsup  11898  xrmaxadd  11901  xrlemininf  11911  xrminltinf  11912  climuni  11933  mulcn2  11952  fsumsplitsnun  12060  prodfap0  12186  fprodabs  12257  efsub  12322  cos12dec  12409  dvdsmodexp  12436  summodnegmod  12463  divalglemex  12563  divalg  12565  modremain  12570  ndvdssub  12571  fldivndvdslt  12578  bitsfzo  12596  nndvdslegcd  12616  dfgcd2  12665  mulgcd  12667  mulgcdr  12669  gcddiv  12670  rplpwr  12678  rppwr  12679  qredeq  12748  divgcdcoprmex  12754  cncongr1  12755  cncongr2  12756  pw2dvdslemn  12817  hashgcdlem  12890  modprm0  12907  modprmn0modprm0  12909  pythagtriplem1  12918  pythagtriplem3  12920  pythagtriplem10  12922  pythagtriplem6  12923  pythagtriplem7  12924  pythagtriplem11  12927  pythagtriplem12  12928  pythagtriplem13  12929  pythagtriplem14  12930  pythagtriplem19  12935  pythagtrip  12936  dvdsprmpweqnn  12989  difsqpwdvds  12991  pcfaclem  13002  pcbc  13004  unennn  13098  ptex  13427  imasaddvallemg  13478  fvprif  13506  mgmsscl  13524  insubm  13648  mulginvcom  13814  mulgassr  13827  mulgmodid  13828  quselbasg  13897  ghmnsgima  13935  ringrng  14130  rmodislmodlem  14446  rmodislmod  14447  lssincl  14481  sralmod  14546  rnglidlmmgm  14592  rnglidlmsgrp  14593  rnglidlrng  14594  2idlcpblrng  14619  psrbaglesuppg  14768  ntrin  14935  elnei  14963  restco  14985  cnpnei  15030  cncnp2m  15042  sslm  15058  upxp  15083  blres  15245  metcnp3  15322  tgqioo  15366  dvply1  15576  ptolemy  15635  cxpcom  15749  logbgcd1irr  15778  logbprmirr  15783  pellexlem1  15791  lgslem1  15819  lgsneg  15843  lgsdilem  15846  lgsdir  15854  lgssq2  15860  lgsdirnn0  15866  gausslemma2dlem1a  15877  2lgslem1a1  15905  incistruhgr  16031  upgrex  16044  uhgr2edg  16147  usgr2v1e2w  16187  issubgr2  16199  0uhgrsubgr  16206  subgrfun  16208  subgreldmiedg  16210  subumgredg2en  16212  iedginwlk  16298  uspgr2wlkeq2  16307  umgrclwwlkge2  16343  clwwlkext2edg  16363  clwwlknccat  16364  umgr2cwwk2dif  16365  umgr2cwwkdifex  16366  clwwlknonex2  16380  gfsumsn  16814