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  2842  vtoclgft  2867  vtoclegft  2891  ifbothdc  3659  ifnebibdc  3670  frirrg  4473  elirr  4665  en2lp  4678  reg3exmidlemwe  4703  sotri3  5163  funtpg  5409  fnprg  5413  fntpg  5414  funimaexglem  5441  fnco  5468  fresaunres2disj  5547  fvun1  5745  oprssov  6198  caovimo  6250  suppsnopdc  6452  funsssuppss  6460  rdgivallem  6614  fnsnsplitdc  6740  funresdfunsndc  6741  mapsnd  6925  f1dom2g  6997  mapxpen  7103  ssfidc  7200  sbthlemi4  7232  ordiso2  7328  updjud  7375  difinfsn  7393  mkvprop  7451  endjudisj  7519  distrnqg  7704  distrnq0  7776  prarloclem5  7817  cauappcvgprlemlol  7964  cauappcvgprlemupu  7966  caucvgprlemlol  7987  caucvgprlemupu  7989  caucvgprprlemlol  8015  caucvgprprlemupu  8017  cnegexlem2  8451  apcotr  8883  apadd1  8884  mulext1  8888  div2negap  9011  ltdiv2  9163  nndivtr  9281  difgtsumgt  9649  zdivmul  9671  gtndiv  9676  fzind  9696  eluzuzle  9865  eluzp1p1  9883  peano2uz  9918  qdivcl  9978  irrmul  9982  ledivge1le  10062  xrre2  10157  xaddass  10205  xltadd1  10212  xlt2add  10216  ubioc1  10265  ubicc2  10321  zltaddlt1le  10344  uzsubsubfz  10384  elfz1b  10428  fzp1nel  10442  fz0fzdiffz0  10468  difelfzle  10472  elfzo0  10524  elfzonlteqm1  10559  fzonn0p1p1  10562  fzosplitprm1  10584  fzoshftral  10588  subfzo0  10592  ceiqle  10679  modqval  10690  modqvalr  10691  flqpmodeq  10693  modq0  10695  mulqmod0  10696  negqmod0  10697  modqge0  10698  modqlt  10699  modqelico  10700  modqdiffl  10701  modqmulnn  10708  modqvalp1  10709  modqmuladdnn0  10734  qnegmod  10735  addmodid  10738  q2submod  10751  modifeq2int  10752  modfzo0difsn  10761  addmodlteq  10764  mulsubdivbinom2ap  11077  omgadd  11170  hashun  11173  ccatass  11300  lswccatn0lsw  11303  ccats1val2  11332  swrd00g  11345  swrdval2  11347  swrdlen  11348  swrdfv  11349  swrdfv0  11350  swrdnd  11355  swrdlen2  11358  swrdfv2  11359  swrdsbslen  11362  swrdspsleq  11363  ccatswrd  11366  pfxfv  11380  pfxn0  11384  pfxnd  11385  pfxsuff1eqwrdeq  11395  pfxpfx  11404  ccats1pfxeq  11410  ccatopth2  11413  wrd2ind  11419  pfxccatin12lem3  11428  pfxccat3  11430  swrdccat  11431  pfxccat3a  11434  redivap  11563  imdivap  11570  xrmaxltsup  11947  xrmaxadd  11950  xrlemininf  11960  xrminltinf  11961  climuni  11982  mulcn2  12001  fsumsplitsnun  12109  prodfap0  12235  fprodabs  12306  efsub  12371  cos12dec  12458  dvdsmodexp  12485  summodnegmod  12512  divalglemex  12612  divalg  12614  modremain  12619  ndvdssub  12620  fldivndvdslt  12627  bitsfzo  12645  nndvdslegcd  12665  dfgcd2  12714  mulgcd  12716  mulgcdr  12718  gcddiv  12719  rplpwr  12727  rppwr  12728  qredeq  12797  divgcdcoprmex  12803  cncongr1  12804  cncongr2  12805  pw2dvdslemn  12866  hashgcdlem  12939  modprm0  12956  modprmn0modprm0  12958  pythagtriplem1  12967  pythagtriplem3  12969  pythagtriplem10  12971  pythagtriplem6  12972  pythagtriplem7  12973  pythagtriplem11  12976  pythagtriplem12  12977  pythagtriplem13  12978  pythagtriplem14  12979  pythagtriplem19  12984  pythagtrip  12985  dvdsprmpweqnn  13038  difsqpwdvds  13040  pcfaclem  13051  pcbc  13053  unennn  13165  ptex  13494  imasaddvallemg  13545  fvprif  13573  mgmsscl  13591  insubm  13715  mulginvcom  13881  mulgassr  13894  mulgmodid  13895  quselbasg  13964  ghmnsgima  14002  ringrng  14197  rmodislmodlem  14515  rmodislmod  14516  lssincl  14550  sralmod  14615  rnglidlmmgm  14661  rnglidlmsgrp  14662  rnglidlrng  14663  2idlcpblrng  14688  psrbaglesuppg  14838  psrbagaddclfi  14842  ntrin  15006  elnei  15034  restco  15056  cnpnei  15101  cncnp2m  15113  sslm  15129  upxp  15154  blres  15316  metcnp3  15393  tgqioo  15437  dvply1  15647  ptolemy  15706  cxpcom  15820  logbgcd1irr  15849  logbprmirr  15854  pellexlem1  15862  lgslem1  15890  lgsneg  15914  lgsdilem  15917  lgsdir  15925  lgssq2  15931  lgsdirnn0  15937  gausslemma2dlem1a  15948  2lgslem1a1  15976  incistruhgr  16102  upgrex  16115  uhgr2edg  16218  usgr2v1e2w  16258  issubgr2  16270  0uhgrsubgr  16277  subgrfun  16279  subgreldmiedg  16281  subumgredg2en  16283  iedginwlk  16369  uspgr2wlkeq2  16378  umgrclwwlkge2  16414  clwwlkext2edg  16434  clwwlknccat  16435  umgr2cwwk2dif  16436  umgr2cwwkdifex  16437  clwwlknonex2  16451  gfsumsn  16884