Theorem 3ad2ant1 1021

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 1019	1 |- ( ( ph /\ ps /\ 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:  simp1l  1024  simp1r  1025  simp11  1030  simp12  1031  simp13  1032  simp1ll  1063  simp1lr  1064  simp1rl  1065  simp1rr  1066  simp1l1  1093  simp1l2  1094  simp1l3  1095  simp1r1  1096  simp1r2  1097  simp1r3  1098  simp11l  1111  simp11r  1112  simp12l  1113  simp12r  1114  simp13l  1115  simp13r  1116  simp111  1129  simp112  1130  simp113  1131  simp121  1132  simp122  1133  simp123  1134  simp131  1135  simp132  1136  simp133  1137  3anim123i  1187  3jaao  1321  ceqsalt  2798  sbciegft  3029  reupick2  3459  ifbothdc  3605  frirrg  4398  breldmg  4885  fntpg  5331  funimaexglem  5358  fex2  5446  fvun1  5647  fprg  5769  fsnunfv  5787  fnfvima  5821  cocan1  5858  cocan2  5859  mpoeq3dv  6013  fovcld  6052  fvmpopr2d  6084  funexw  6199  mpofvex  6293  poxp  6320  smoiso  6390  tfrlem5  6402  tfrlemibxssdm  6415  tfr1onlembfn  6432  tfri1dALT  6439  tfrcllembfn  6445  rdgon  6474  freccllem  6490  nnawordex  6617  mapxpen  6947  fidceq  6968  fidifsnen  6969  dif1en  6978  en2eqpr  7006  unsnfi  7018  unsnfidcex  7019  unsnfidcel  7020  fisseneq  7033  ordiso2  7139  updjud  7186  mkvprop  7262  endjudisj  7324  xpdjuen  7332  mulcanenq0ec  7560  prltlu  7602  prarloclem3step  7611  prarloclem5  7615  ltasrg  7885  cnegexlem1  8249  addcan  8254  apcotr  8682  apadd1  8683  mulext1  8687  divdivap1  8798  divdivap2  8799  div2negap  8810  divneg2ap  8811  ltmulgt11  8939  ltdiv2  8962  squeeze0  8979  nndivtr  9080  nn0n0n1ge2  9445  zdivmul  9465  gtndiv  9470  eluzuzle  9658  eluzp1p1  9676  qdivcl  9766  irrmul  9770  rpgecl  9806  xaddass  9993  xltadd1  10000  xlt2add  10004  lbico1  10054  lbicc2  10108  zltaddlt1le  10131  uzsubsubfz  10171  elfz1b  10214  elfz0ubfz0  10249  fz0fzelfz0  10251  difelfzle  10258  difelfznle  10259  2ffzeq  10265  fzo1fzo0n0  10309  ubmelfzo  10331  fzonn0p1p1  10344  elfzom1p1elfzo  10345  elfzonelfzo  10361  subfzo0  10373  ceiqle  10460  ceilqle  10461  modqval  10471  flqpmodeq  10474  modq0  10476  negqmod0  10478  modqge0  10479  modqlt  10480  modqdiffl  10482  modqmulnn  10489  modqvalp1  10490  modqmuladdnn0  10515  qnegmod  10516  addmodid  10519  modfzo0difsn  10542  addmodlteq  10545  qexpclz  10707  expgt1  10724  expp1zap  10735  expm1ap  10736  expubnd  10743  bernneq2  10808  expnlbnd  10811  mulsubdivbinom2ap  10858  omgadd  10949  hashun  10952  fihashssdif  10965  hashdifpr  10967  fimaxq  10974  ccatval2  11057  ccatval3  11058  ccatval1lsw  11063  ccatval21sw  11064  ccatass  11067  ccats1val2  11095  fzowrddc  11103  swrdval  11104  swrdclg  11106  swrdval2  11107  swrdnd  11115  swrdlen2  11118  swrdfv2  11119  ccatswrd  11126  pfxn0  11142  pfxsuff1eqwrdeq  11153  shftuz  11161  mulreap  11208  redivap  11218  imdivap  11225  resqrtcl  11373  xrmaxltsup  11602  xrmaxaddlem  11604  xrmaxadd  11605  xrlemininf  11615  xrminltinf  11616  climuni  11637  addcn2  11654  mulcn2  11656  efsub  12025  sin02gt0  12108  cos12dec  12112  dvdsval2  12134  addmodlteqALT  12203  modremain  12273  fldivndvdslt  12281  mulgcdr  12372  gcddiv  12373  rpmulgcd  12380  rplpwr  12381  rppwr  12382  nnminle  12389  qredeq  12451  divgcdcoprmex  12457  cncongr1  12458  cncongr2  12459  dvdsnprmd  12480  euclemma  12501  prmexpb  12506  qnumdenbi  12547  eulerth  12588  fermltl  12589  prmdiv  12590  hashgcdlem  12593  odzcllem  12598  vfermltl  12607  reumodprminv  12609  modprm0  12610  modprmn0modprm0  12612  coprimeprodsq  12613  pythagtriplem1  12621  pythagtriplem3  12623  pythagtriplem4  12624  pythagtriplem10  12625  pythagtriplem6  12626  pythagtriplem7  12627  pythagtriplem8  12628  pythagtriplem9  12629  pythagtriplem11  12630  pythagtriplem12  12631  pythagtriplem13  12632  pythagtriplem14  12633  pythagtriplem15  12634  pythagtriplem16  12635  pythagtriplem17  12636  pythagtriplem19  12638  pythagtrip  12639  pcpremul  12649  pcdvdsb  12676  dvdsprmpweqnn  12692  dvdsprmpweqle  12693  difsqpwdvds  12694  pcfaclem  12705  pcbc  12707  4sqlem12  12758  unennn  12801  nninfdc  12857  setsex  12897  f1ocpbllem  13175  imasaddfnlemg  13179  imasaddvallemg  13180  ercpbl  13196  erlecpbl  13197  qusaddvallemg  13198  fvprif  13208  xpsfrnel2  13211  plusfvalg  13228  imasmnd  13318  insubm  13350  grpidrcan  13430  grpidlcan  13431  grpsubpropd2  13470  pwsinvg  13477  imasgrp2  13479  imasgrp  13480  mulgnnsubcl  13503  mulgnn0subcl  13504  mulgsubcl  13505  mulgaddcom  13515  mulginvcom  13516  mulgnnass  13526  mulgassr  13529  mulgpropdg  13533  submmulg  13535  subgcl  13553  subgsubcl  13554  subgsub  13555  subgmulg  13557  nsgconj  13575  ghmsub  13620  ghmrn  13626  ghmeqker  13640  f1ghm0to0  13641  ablinvadd  13679  ablsub4  13682  abladdsub4  13683  subcmnd  13702  imasabl  13705  rngcl  13739  imasrng  13751  srgcl  13765  srg1zr  13782  srgen1zr  13783  ringcl  13808  crngcom  13809  ringidss  13824  mulgass2  13853  imasring  13859  opprmulg  13866  unitmulclb  13909  unitdvcl  13931  rhmmul  13959  rhmdvdsr  13970  subrngmcl  14004  subrgmcl  14028  subrgdv  14033  subrgugrp  14035  domneq0  14067  scafvalg  14102  lmodprop2d  14143  lssclg  14159  lssvnegcl  14171  lssintclm  14179  sralmod  14245  rnglidlmcl  14275  lidlnegcl  14280  rspssp  14289  rnglidlmsgrp  14292  rnglidlrng  14293  2idlcpblrng  14318  qus2idrng  14320  zndvds  14444  znleval2  14449  basgen  14585  2basgeng  14587  iuncld  14620  neipsm  14659  opnneissb  14660  opnssneib  14661  iscnp3  14708  cnprcl2k  14711  cnpnei  14724  cncnp2m  14736  cnptoprest  14744  sslm  14752  upxp  14777  cnmpt22  14799  distspace  14840  0met  14889  blvalps  14893  blval  14894  ssblps  14930  ssbl  14931  blpnfctr  14944  blopn  14995  blnei  14997  bdxmet  15006  bdbl  15008  metcnp3  15016  tgqioo  15060  ptolemy  15329  sinq12gt0  15335  sincosq1eq  15344  rpcxpadd  15410  cxpmul  15417  rplogbval  15450  logbleb  15466  logbgcd1irr  15472  logbprmirr  15477  lgsfvalg  15515  lgsneg1  15535  lgssq  15550  lgsdinn0  15558  gausslemma2dlem1a  15568  2lgs  15614  2lgsoddprmlem2  15616  funvtxdm2domval  15659  funiedgdm2domval  15660  iedgedgg  15688  bdfind  15919  1dom1el  15964