Theorem 3ad2ant1 1020

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

Syntax hints:   -> wi 4   /\ w3a 980

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 982

This theorem is referenced by:  simp1l  1023  simp1r  1024  simp11  1029  simp12  1030  simp13  1031  simp1ll  1062  simp1lr  1063  simp1rl  1064  simp1rr  1065  simp1l1  1092  simp1l2  1093  simp1l3  1094  simp1r1  1095  simp1r2  1096  simp1r3  1097  simp11l  1110  simp11r  1111  simp12l  1112  simp12r  1113  simp13l  1114  simp13r  1115  simp111  1128  simp112  1129  simp113  1130  simp121  1131  simp122  1132  simp123  1133  simp131  1134  simp132  1135  simp133  1136  3anim123i  1186  3jaao  1319  ceqsalt  2782  sbciegft  3012  reupick2  3440  ifbothdc  3586  frirrg  4375  breldmg  4858  fntpg  5298  funimaexglem  5325  fex2  5410  fvun1  5610  fprg  5727  fsnunfv  5745  fnfvima  5779  cocan1  5816  cocan2  5817  mpoeq3dv  5970  fovcld  6009  funexw  6145  mpofvex  6236  poxp  6265  smoiso  6335  tfrlem5  6347  tfrlemibxssdm  6360  tfr1onlembfn  6377  tfri1dALT  6384  tfrcllembfn  6390  rdgon  6419  freccllem  6435  nnawordex  6562  mapxpen  6884  fidceq  6905  fidifsnen  6906  dif1en  6915  en2eqpr  6943  unsnfi  6955  unsnfidcex  6956  unsnfidcel  6957  fisseneq  6968  ordiso2  7073  updjud  7120  mkvprop  7196  endjudisj  7249  xpdjuen  7257  mulcanenq0ec  7484  prltlu  7526  prarloclem3step  7535  prarloclem5  7539  ltasrg  7809  cnegexlem1  8173  addcan  8178  apcotr  8605  apadd1  8606  mulext1  8610  divdivap1  8721  divdivap2  8722  div2negap  8733  divneg2ap  8734  ltmulgt11  8862  ltdiv2  8885  squeeze0  8902  nndivtr  9002  nn0n0n1ge2  9364  zdivmul  9384  gtndiv  9389  eluzuzle  9577  eluzp1p1  9595  qdivcl  9685  irrmul  9689  rpgecl  9724  xaddass  9911  xltadd1  9918  xlt2add  9922  lbico1  9972  lbicc2  10026  zltaddlt1le  10049  uzsubsubfz  10089  elfz1b  10132  elfz0ubfz0  10167  fz0fzelfz0  10169  difelfzle  10176  difelfznle  10177  2ffzeq  10183  fzo1fzo0n0  10225  ubmelfzo  10242  fzonn0p1p1  10255  elfzom1p1elfzo  10256  elfzonelfzo  10272  subfzo0  10284  ceiqle  10356  ceilqle  10357  modqval  10367  flqpmodeq  10370  modq0  10372  negqmod0  10374  modqge0  10375  modqlt  10376  modqdiffl  10378  modqmulnn  10385  modqvalp1  10386  modqmuladdnn0  10411  qnegmod  10412  addmodid  10415  modfzo0difsn  10438  addmodlteq  10441  qexpclz  10587  expgt1  10604  expp1zap  10615  expm1ap  10616  expubnd  10623  bernneq2  10688  expnlbnd  10691  mulsubdivbinom2ap  10738  omgadd  10829  hashun  10832  fihashssdif  10845  hashdifpr  10847  fimaxq  10854  shftuz  10873  mulreap  10920  redivap  10930  imdivap  10937  resqrtcl  11085  xrmaxltsup  11313  xrmaxaddlem  11315  xrmaxadd  11316  xrlemininf  11326  xrminltinf  11327  climuni  11348  addcn2  11365  mulcn2  11367  efsub  11736  sin02gt0  11818  cos12dec  11822  dvdsval2  11844  addmodlteqALT  11912  modremain  11981  fldivndvdslt  11987  mulgcdr  12066  gcddiv  12067  rpmulgcd  12074  rplpwr  12075  rppwr  12076  nnminle  12083  qredeq  12145  divgcdcoprmex  12151  cncongr1  12152  cncongr2  12153  dvdsnprmd  12174  euclemma  12195  prmexpb  12200  qnumdenbi  12241  eulerth  12282  fermltl  12283  prmdiv  12284  hashgcdlem  12287  odzcllem  12291  vfermltl  12300  reumodprminv  12302  modprm0  12303  modprmn0modprm0  12305  coprimeprodsq  12306  pythagtriplem1  12314  pythagtriplem3  12316  pythagtriplem4  12317  pythagtriplem10  12318  pythagtriplem6  12319  pythagtriplem7  12320  pythagtriplem8  12321  pythagtriplem9  12322  pythagtriplem11  12323  pythagtriplem12  12324  pythagtriplem13  12325  pythagtriplem14  12326  pythagtriplem15  12327  pythagtriplem16  12328  pythagtriplem17  12329  pythagtriplem19  12331  pythagtrip  12332  pcpremul  12342  pcdvdsb  12369  dvdsprmpweqnn  12385  dvdsprmpweqle  12386  difsqpwdvds  12387  pcfaclem  12398  pcbc  12400  4sqlem12  12451  unennn  12465  nninfdc  12521  setsex  12561  f1ocpbllem  12804  imasaddfnlemg  12808  imasaddvallemg  12809  ercpbl  12825  erlecpbl  12826  qusaddvallemg  12827  fvprif  12837  xpsfrnel2  12840  plusfvalg  12857  insubm  12967  grpidrcan  13040  grpidlcan  13041  grpsubpropd2  13080  imasgrp2  13083  imasgrp  13084  mulgnnsubcl  13107  mulgnn0subcl  13108  mulgsubcl  13109  mulgaddcom  13119  mulginvcom  13120  mulgnnass  13130  mulgassr  13133  mulgpropdg  13137  subgcl  13156  subgsubcl  13157  subgsub  13158  subgmulg  13160  nsgconj  13178  ghmsub  13223  ghmrn  13229  ghmeqker  13243  f1ghm0to0  13244  ablinvadd  13282  ablsub4  13285  abladdsub4  13286  subcmnd  13305  imasabl  13308  rngcl  13333  imasrng  13345  srgcl  13359  srg1zr  13376  srgen1zr  13377  ringcl  13402  crngcom  13403  ringidss  13418  mulgass2  13445  imasring  13451  opprmulg  13458  unitmulclb  13501  unitdvcl  13523  rhmmul  13551  rhmdvdsr  13562  subrngmcl  13593  subrgmcl  13617  subrgdv  13622  subrgugrp  13624  scafvalg  13666  lmodprop2d  13707  lssclg  13723  lssvnegcl  13735  lssintclm  13743  sralmod  13809  rnglidlmcl  13839  lidlnegcl  13844  rspssp  13853  rnglidlmsgrp  13856  rnglidlrng  13857  2idlcpblrng  13882  qus2idrng  13884  zndvds  13993  znleval2  13998  basgen  14101  2basgeng  14103  iuncld  14136  neipsm  14175  opnneissb  14176  opnssneib  14177  iscnp3  14224  cnprcl2k  14227  cnpnei  14240  cncnp2m  14252  cnptoprest  14260  sslm  14268  upxp  14293  cnmpt22  14315  distspace  14356  0met  14405  blvalps  14409  blval  14410  ssblps  14446  ssbl  14447  blpnfctr  14460  blopn  14511  blnei  14513  bdxmet  14522  bdbl  14524  metcnp3  14532  tgqioo  14568  ptolemy  14783  sinq12gt0  14789  sincosq1eq  14798  rpcxpadd  14864  cxpmul  14871  rplogbval  14901  logbleb  14917  logbgcd1irr  14923  logbprmirr  14928  lgsfvalg  14945  lgsneg1  14965  lgssq  14980  lgsdinn0  14988  2lgsoddprmlem2  14993  bdfind  15237  1dom1el  15282