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  2803  vtoclgft  2828  vtoclegft  2852  ifbothdc  3614  ifnebibdc  3625  frirrg  4415  elirr  4607  en2lp  4620  reg3exmidlemwe  4645  sotri3  5100  funtpg  5344  fnprg  5348  fntpg  5349  funimaexglem  5376  fnco  5403  fvun1  5668  oprssov  6111  caovimo  6163  rdgivallem  6490  fnsnsplitdc  6614  funresdfunsndc  6615  f1dom2g  6870  mapxpen  6970  ssfidc  7060  sbthlemi4  7088  ordiso2  7163  updjud  7210  difinfsn  7228  mkvprop  7286  endjudisj  7353  distrnqg  7535  distrnq0  7607  prarloclem5  7648  cauappcvgprlemlol  7795  cauappcvgprlemupu  7797  caucvgprlemlol  7818  caucvgprlemupu  7820  caucvgprprlemlol  7846  caucvgprprlemupu  7848  cnegexlem2  8283  apcotr  8715  apadd1  8716  mulext1  8720  div2negap  8843  ltdiv2  8995  nndivtr  9113  difgtsumgt  9477  zdivmul  9498  gtndiv  9503  fzind  9523  eluzuzle  9691  eluzp1p1  9709  peano2uz  9739  qdivcl  9799  irrmul  9803  ledivge1le  9883  xrre2  9978  xaddass  10026  xltadd1  10033  xlt2add  10037  ubioc1  10086  ubicc2  10142  zltaddlt1le  10164  uzsubsubfz  10204  elfz1b  10247  fzp1nel  10261  fz0fzdiffz0  10287  difelfzle  10291  elfzo0  10343  elfzonlteqm1  10376  fzonn0p1p1  10379  fzosplitprm1  10400  fzoshftral  10404  subfzo0  10408  ceiqle  10495  modqval  10506  modqvalr  10507  flqpmodeq  10509  modq0  10511  mulqmod0  10512  negqmod0  10513  modqge0  10514  modqlt  10515  modqelico  10516  modqdiffl  10517  modqmulnn  10524  modqvalp1  10525  modqmuladdnn0  10550  qnegmod  10551  addmodid  10554  q2submod  10567  modifeq2int  10568  modfzo0difsn  10577  addmodlteq  10580  mulsubdivbinom2ap  10893  omgadd  10984  hashun  10987  ccatass  11102  lswccatn0lsw  11105  ccats1val2  11130  swrd00g  11140  swrdval2  11142  swrdlen  11143  swrdfv  11144  swrdfv0  11145  swrdnd  11150  swrdlen2  11153  swrdfv2  11154  swrdsbslen  11157  swrdspsleq  11158  ccatswrd  11161  pfxfv  11175  pfxn0  11179  pfxnd  11180  pfxsuff1eqwrdeq  11190  pfxpfx  11199  ccats1pfxeq  11205  ccatopth2  11208  wrd2ind  11214  pfxccatin12lem3  11223  pfxccat3  11225  swrdccat  11226  pfxccat3a  11229  redivap  11300  imdivap  11307  xrmaxltsup  11684  xrmaxadd  11687  xrlemininf  11697  xrminltinf  11698  climuni  11719  mulcn2  11738  fsumsplitsnun  11845  prodfap0  11971  fprodabs  12042  efsub  12107  cos12dec  12194  dvdsmodexp  12221  summodnegmod  12248  divalglemex  12348  divalg  12350  modremain  12355  ndvdssub  12356  fldivndvdslt  12363  bitsfzo  12381  nndvdslegcd  12401  dfgcd2  12450  mulgcd  12452  mulgcdr  12454  gcddiv  12455  rplpwr  12463  rppwr  12464  qredeq  12533  divgcdcoprmex  12539  cncongr1  12540  cncongr2  12541  pw2dvdslemn  12602  hashgcdlem  12675  modprm0  12692  modprmn0modprm0  12694  pythagtriplem1  12703  pythagtriplem3  12705  pythagtriplem10  12707  pythagtriplem6  12708  pythagtriplem7  12709  pythagtriplem11  12712  pythagtriplem12  12713  pythagtriplem13  12714  pythagtriplem14  12715  pythagtriplem19  12720  pythagtrip  12721  dvdsprmpweqnn  12774  difsqpwdvds  12776  pcfaclem  12787  pcbc  12789  unennn  12883  ptex  13211  imasaddvallemg  13262  fvprif  13290  mgmsscl  13308  insubm  13432  mulginvcom  13598  mulgassr  13611  mulgmodid  13612  quselbasg  13681  ghmnsgima  13719  ringrng  13913  rmodislmodlem  14227  rmodislmod  14228  lssincl  14262  sralmod  14327  rnglidlmmgm  14373  rnglidlmsgrp  14374  rnglidlrng  14375  2idlcpblrng  14400  psrbaglesuppg  14549  ntrin  14711  elnei  14739  restco  14761  cnpnei  14806  cncnp2m  14818  sslm  14834  upxp  14859  blres  15021  metcnp3  15098  tgqioo  15142  dvply1  15352  ptolemy  15411  cxpcom  15525  logbgcd1irr  15554  logbprmirr  15559  lgslem1  15592  lgsneg  15616  lgsdilem  15619  lgsdir  15627  lgssq2  15633  lgsdirnn0  15639  gausslemma2dlem1a  15650  2lgslem1a1  15678  incistruhgr  15801  upgrex  15814