Theorem 3ad2ant1 1042

Description: Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)

Hypothesis

Ref	Expression
3ad2ant.1	|- ( ph -> ch )

Assertion

Ref	Expression
3ad2ant1	|- ( ( ph /\ ps /\ th ) -> ch )

Proof of Theorem 3ad2ant1

Step	Hyp	Ref	Expression
1		3ad2ant.1	. . 3 |- ( ph -> ch )
2	1	adantr 276	. 2 |- ( ( ph /\ th ) -> ch )
3	2	3adant2 1040	1 |- ( ( ph /\ ps /\ 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:  simp1l  1045  simp1r  1046  simp11  1051  simp12  1052  simp13  1053  simp1ll  1084  simp1lr  1085  simp1rl  1086  simp1rr  1087  simp1l1  1114  simp1l2  1115  simp1l3  1116  simp1r1  1117  simp1r2  1118  simp1r3  1119  simp11l  1132  simp11r  1133  simp12l  1134  simp12r  1135  simp13l  1136  simp13r  1137  simp111  1150  simp112  1151  simp113  1152  simp121  1153  simp122  1154  simp123  1155  simp131  1156  simp132  1157  simp133  1158  3anim123i  1208  3jaao  1342  ceqsalt  2826  sbciegft  3059  reupick2  3490  ifbothdc  3637  frirrg  4441  breldmg  4929  fntpg  5377  funimaexglem  5404  fex2  5492  fvun1  5700  fprg  5822  fsnunfv  5840  fnfvima  5874  cocan1  5911  cocan2  5912  mpoeq3dv  6070  fovcld  6109  fvmpopr2d  6141  funexw  6257  mpofvex  6351  poxp  6378  smoiso  6448  tfrlem5  6460  tfrlemibxssdm  6473  tfr1onlembfn  6490  tfri1dALT  6497  tfrcllembfn  6503  rdgon  6532  freccllem  6548  nnawordex  6675  mapxpen  7009  fidceq  7031  fidifsnen  7032  dif1en  7041  en2eqpr  7069  unsnfi  7081  unsnfidcex  7082  unsnfidcel  7083  fisseneq  7096  ordiso2  7202  updjud  7249  mkvprop  7325  endjudisj  7392  xpdjuen  7400  mulcanenq0ec  7632  prltlu  7674  prarloclem3step  7683  prarloclem5  7687  ltasrg  7957  cnegexlem1  8321  addcan  8326  apcotr  8754  apadd1  8755  mulext1  8759  divdivap1  8870  divdivap2  8871  div2negap  8882  divneg2ap  8883  ltmulgt11  9011  ltdiv2  9034  squeeze0  9051  nndivtr  9152  nn0n0n1ge2  9517  zdivmul  9537  gtndiv  9542  eluzuzle  9730  eluzp1p1  9748  qdivcl  9838  irrmul  9842  rpgecl  9878  xaddass  10065  xltadd1  10072  xlt2add  10076  lbico1  10126  lbicc2  10180  zltaddlt1le  10203  uzsubsubfz  10243  elfz1b  10286  elfz0ubfz0  10321  fz0fzelfz0  10323  difelfzle  10330  difelfznle  10331  2ffzeq  10337  fzo1fzo0n0  10383  ubmelfzo  10406  fzonn0p1p1  10419  elfzom1p1elfzo  10420  elfzonelfzo  10436  subfzo0  10448  ceiqle  10535  ceilqle  10536  modqval  10546  flqpmodeq  10549  modq0  10551  negqmod0  10553  modqge0  10554  modqlt  10555  modqdiffl  10557  modqmulnn  10564  modqvalp1  10565  modqmuladdnn0  10590  qnegmod  10591  addmodid  10594  modfzo0difsn  10617  addmodlteq  10620  qexpclz  10782  expgt1  10799  expp1zap  10810  expm1ap  10811  expubnd  10818  bernneq2  10883  expnlbnd  10886  mulsubdivbinom2ap  10933  omgadd  11024  hashun  11027  fihashssdif  11040  hashdifpr  11042  fimaxq  11049  ccatval2  11133  ccatval3  11134  ccatval1lsw  11139  ccatval21sw  11140  ccatass  11143  ccats1val2  11171  fzowrddc  11179  swrdval  11180  swrdclg  11182  swrdval2  11183  swrdnd  11191  swrdlen2  11194  swrdfv2  11195  ccatswrd  11202  pfxn0  11220  pfxsuff1eqwrdeq  11231  swrdswrdlem  11236  ccats1pfxeq  11246  ccats1pfxeqrex  11247  ccatopth2  11249  wrd2ind  11255  pfxccatin12lem3  11264  pfxccat3  11266  swrdccat  11267  pfxccatpfx2  11269  pfxccat3a  11270  swrdccat3b  11272  pfxccatid  11273  ccats1pfxeqbi  11274  shftuz  11328  mulreap  11375  redivap  11385  imdivap  11392  resqrtcl  11540  xrmaxltsup  11769  xrmaxaddlem  11771  xrmaxadd  11772  xrlemininf  11782  xrminltinf  11783  climuni  11804  addcn2  11821  mulcn2  11823  efsub  12192  sin02gt0  12275  cos12dec  12279  dvdsval2  12301  addmodlteqALT  12370  modremain  12440  fldivndvdslt  12448  mulgcdr  12539  gcddiv  12540  rpmulgcd  12547  rplpwr  12548  rppwr  12549  nnminle  12556  qredeq  12618  divgcdcoprmex  12624  cncongr1  12625  cncongr2  12626  dvdsnprmd  12647  euclemma  12668  prmexpb  12673  qnumdenbi  12714  eulerth  12755  fermltl  12756  prmdiv  12757  hashgcdlem  12760  odzcllem  12765  vfermltl  12774  reumodprminv  12776  modprm0  12777  modprmn0modprm0  12779  coprimeprodsq  12780  pythagtriplem1  12788  pythagtriplem3  12790  pythagtriplem4  12791  pythagtriplem10  12792  pythagtriplem6  12793  pythagtriplem7  12794  pythagtriplem8  12795  pythagtriplem9  12796  pythagtriplem11  12797  pythagtriplem12  12798  pythagtriplem13  12799  pythagtriplem14  12800  pythagtriplem15  12801  pythagtriplem16  12802  pythagtriplem17  12803  pythagtriplem19  12805  pythagtrip  12806  pcpremul  12816  pcdvdsb  12843  dvdsprmpweqnn  12859  dvdsprmpweqle  12860  difsqpwdvds  12861  pcfaclem  12872  pcbc  12874  4sqlem12  12925  unennn  12968  nninfdc  13024  setsex  13064  f1ocpbllem  13343  imasaddfnlemg  13347  imasaddvallemg  13348  ercpbl  13364  erlecpbl  13365  qusaddvallemg  13366  fvprif  13376  xpsfrnel2  13379  plusfvalg  13396  imasmnd  13486  insubm  13518  grpidrcan  13598  grpidlcan  13599  grpsubpropd2  13638  pwsinvg  13645  imasgrp2  13647  imasgrp  13648  mulgnnsubcl  13671  mulgnn0subcl  13672  mulgsubcl  13673  mulgaddcom  13683  mulginvcom  13684  mulgnnass  13694  mulgassr  13697  mulgpropdg  13701  submmulg  13703  subgcl  13721  subgsubcl  13722  subgsub  13723  subgmulg  13725  nsgconj  13743  ghmsub  13788  ghmrn  13794  ghmeqker  13808  f1ghm0to0  13809  ablinvadd  13847  ablsub4  13850  abladdsub4  13851  subcmnd  13870  imasabl  13873  rngcl  13907  imasrng  13919  srgcl  13933  srg1zr  13950  srgen1zr  13951  ringcl  13976  crngcom  13977  ringidss  13992  mulgass2  14021  imasring  14027  opprmulg  14034  unitmulclb  14078  unitdvcl  14100  rhmmul  14128  rhmdvdsr  14139  subrngmcl  14173  subrgmcl  14197  subrgdv  14202  subrgugrp  14204  domneq0  14236  scafvalg  14271  lmodprop2d  14312  lssclg  14328  lssvnegcl  14340  lssintclm  14348  sralmod  14414  rnglidlmcl  14444  lidlnegcl  14449  rspssp  14458  rnglidlmsgrp  14461  rnglidlrng  14462  2idlcpblrng  14487  qus2idrng  14489  zndvds  14613  znleval2  14618  basgen  14754  2basgeng  14756  iuncld  14789  neipsm  14828  opnneissb  14829  opnssneib  14830  iscnp3  14877  cnprcl2k  14880  cnpnei  14893  cncnp2m  14905  cnptoprest  14913  sslm  14921  upxp  14946  cnmpt22  14968  distspace  15009  0met  15058  blvalps  15062  blval  15063  ssblps  15099  ssbl  15100  blpnfctr  15113  blopn  15164  blnei  15166  bdxmet  15175  bdbl  15177  metcnp3  15185  tgqioo  15229  ptolemy  15498  sinq12gt0  15504  sincosq1eq  15513  rpcxpadd  15579  cxpmul  15586  rplogbval  15619  logbleb  15635  logbgcd1irr  15641  logbprmirr  15646  lgsfvalg  15684  lgsneg1  15704  lgssq  15719  lgsdinn0  15727  gausslemma2dlem1a  15737  2lgs  15783  2lgsoddprmlem2  15785  funvtxdm2domval  15830  funiedgdm2domval  15831  iedgedgg  15861  lpvtx  15879  incistruhgr  15890  ausgrumgrien  15968  ausgrusgrien  15969  umgr2edgneu  16010  ushgredgedg  16024  ushgredgedgloop  16026  iswlk  16036  wlkl1loop  16069  uspgr2wlkeq  16076  bdfind  16309  1dom1el  16354