Theorem 3ad2ant2 1022

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

Syntax hints:   -> wi 4   /\ w3a 981

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 983

This theorem is referenced by:  simp2l  1026  simp2r  1027  simp21  1033  simp22  1034  simp23  1035  simp2ll  1067  simp2lr  1068  simp2rl  1069  simp2rr  1070  simp2l1  1099  simp2l2  1100  simp2l3  1101  simp2r1  1102  simp2r2  1103  simp2r3  1104  simp21l  1117  simp21r  1118  simp22l  1119  simp22r  1120  simp23l  1121  simp23r  1122  simp211  1138  simp212  1139  simp213  1140  simp221  1141  simp222  1142  simp223  1143  simp231  1144  simp232  1145  simp233  1146  3anim123i  1187  3jaao  1321  ceqsalt  2798  vtoclgft  2823  vtoclegft  2845  ifbothdc  3605  ifnebibdc  3615  frirrg  4398  elirr  4590  en2lp  4603  reg3exmidlemwe  4628  sotri3  5082  funtpg  5326  fnprg  5330  fntpg  5331  funimaexglem  5358  fnco  5385  fvun1  5647  oprssov  6090  caovimo  6142  rdgivallem  6469  fnsnsplitdc  6593  funresdfunsndc  6594  f1dom2g  6849  mapxpen  6947  ssfidc  7036  sbthlemi4  7064  ordiso2  7139  updjud  7186  difinfsn  7204  mkvprop  7262  endjudisj  7324  distrnqg  7502  distrnq0  7574  prarloclem5  7615  cauappcvgprlemlol  7762  cauappcvgprlemupu  7764  caucvgprlemlol  7785  caucvgprlemupu  7787  caucvgprprlemlol  7813  caucvgprprlemupu  7815  cnegexlem2  8250  apcotr  8682  apadd1  8683  mulext1  8687  div2negap  8810  ltdiv2  8962  nndivtr  9080  difgtsumgt  9444  zdivmul  9465  gtndiv  9470  fzind  9490  eluzuzle  9658  eluzp1p1  9676  peano2uz  9706  qdivcl  9766  irrmul  9770  ledivge1le  9850  xrre2  9945  xaddass  9993  xltadd1  10000  xlt2add  10004  ubioc1  10053  ubicc2  10109  zltaddlt1le  10131  uzsubsubfz  10171  elfz1b  10214  fzp1nel  10228  fz0fzdiffz0  10254  difelfzle  10258  elfzo0  10308  elfzonlteqm1  10341  fzonn0p1p1  10344  fzosplitprm1  10365  fzoshftral  10369  subfzo0  10373  ceiqle  10460  modqval  10471  modqvalr  10472  flqpmodeq  10474  modq0  10476  mulqmod0  10477  negqmod0  10478  modqge0  10479  modqlt  10480  modqelico  10481  modqdiffl  10482  modqmulnn  10489  modqvalp1  10490  modqmuladdnn0  10515  qnegmod  10516  addmodid  10519  q2submod  10532  modifeq2int  10533  modfzo0difsn  10542  addmodlteq  10545  mulsubdivbinom2ap  10858  omgadd  10949  hashun  10952  ccatass  11067  lswccatn0lsw  11070  ccats1val2  11095  swrd00g  11105  swrdval2  11107  swrdlen  11108  swrdfv  11109  swrdfv0  11110  swrdnd  11115  swrdlen2  11118  swrdfv2  11119  swrdsbslen  11122  swrdspsleq  11123  ccatswrd  11126  pfxfv  11138  pfxn0  11142  pfxnd  11143  pfxsuff1eqwrdeq  11153  redivap  11218  imdivap  11225  xrmaxltsup  11602  xrmaxadd  11605  xrlemininf  11615  xrminltinf  11616  climuni  11637  mulcn2  11656  fsumsplitsnun  11763  prodfap0  11889  fprodabs  11960  efsub  12025  cos12dec  12112  dvdsmodexp  12139  summodnegmod  12166  divalglemex  12266  divalg  12268  modremain  12273  ndvdssub  12274  fldivndvdslt  12281  bitsfzo  12299  nndvdslegcd  12319  dfgcd2  12368  mulgcd  12370  mulgcdr  12372  gcddiv  12373  rplpwr  12381  rppwr  12382  qredeq  12451  divgcdcoprmex  12457  cncongr1  12458  cncongr2  12459  pw2dvdslemn  12520  hashgcdlem  12593  modprm0  12610  modprmn0modprm0  12612  pythagtriplem1  12621  pythagtriplem3  12623  pythagtriplem10  12625  pythagtriplem6  12626  pythagtriplem7  12627  pythagtriplem11  12630  pythagtriplem12  12631  pythagtriplem13  12632  pythagtriplem14  12633  pythagtriplem19  12638  pythagtrip  12639  dvdsprmpweqnn  12692  difsqpwdvds  12694  pcfaclem  12705  pcbc  12707  unennn  12801  ptex  13129  imasaddvallemg  13180  fvprif  13208  mgmsscl  13226  insubm  13350  mulginvcom  13516  mulgassr  13529  mulgmodid  13530  quselbasg  13599  ghmnsgima  13637  ringrng  13831  rmodislmodlem  14145  rmodislmod  14146  lssincl  14180  sralmod  14245  rnglidlmmgm  14291  rnglidlmsgrp  14292  rnglidlrng  14293  2idlcpblrng  14318  psrbaglesuppg  14467  ntrin  14629  elnei  14657  restco  14679  cnpnei  14724  cncnp2m  14736  sslm  14752  upxp  14777  blres  14939  metcnp3  15016  tgqioo  15060  dvply1  15270  ptolemy  15329  cxpcom  15443  logbgcd1irr  15472  logbprmirr  15477  lgslem1  15510  lgsneg  15534  lgsdilem  15537  lgsdir  15545  lgssq2  15551  lgsdirnn0  15557  gausslemma2dlem1a  15568  2lgslem1a1  15596