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  2789  sbciegft  3020  reupick2  3449  ifbothdc  3594  frirrg  4385  breldmg  4872  fntpg  5314  funimaexglem  5341  fex2  5426  fvun1  5627  fprg  5745  fsnunfv  5763  fnfvima  5797  cocan1  5834  cocan2  5835  mpoeq3dv  5988  fovcld  6027  fvmpopr2d  6059  funexw  6169  mpofvex  6263  poxp  6290  smoiso  6360  tfrlem5  6372  tfrlemibxssdm  6385  tfr1onlembfn  6402  tfri1dALT  6409  tfrcllembfn  6415  rdgon  6444  freccllem  6460  nnawordex  6587  mapxpen  6909  fidceq  6930  fidifsnen  6931  dif1en  6940  en2eqpr  6968  unsnfi  6980  unsnfidcex  6981  unsnfidcel  6982  fisseneq  6995  ordiso2  7101  updjud  7148  mkvprop  7224  endjudisj  7277  xpdjuen  7285  mulcanenq0ec  7512  prltlu  7554  prarloclem3step  7563  prarloclem5  7567  ltasrg  7837  cnegexlem1  8201  addcan  8206  apcotr  8634  apadd1  8635  mulext1  8639  divdivap1  8750  divdivap2  8751  div2negap  8762  divneg2ap  8763  ltmulgt11  8891  ltdiv2  8914  squeeze0  8931  nndivtr  9032  nn0n0n1ge2  9396  zdivmul  9416  gtndiv  9421  eluzuzle  9609  eluzp1p1  9627  qdivcl  9717  irrmul  9721  rpgecl  9757  xaddass  9944  xltadd1  9951  xlt2add  9955  lbico1  10005  lbicc2  10059  zltaddlt1le  10082  uzsubsubfz  10122  elfz1b  10165  elfz0ubfz0  10200  fz0fzelfz0  10202  difelfzle  10209  difelfznle  10210  2ffzeq  10216  fzo1fzo0n0  10259  ubmelfzo  10276  fzonn0p1p1  10289  elfzom1p1elfzo  10290  elfzonelfzo  10306  subfzo0  10318  ceiqle  10405  ceilqle  10406  modqval  10416  flqpmodeq  10419  modq0  10421  negqmod0  10423  modqge0  10424  modqlt  10425  modqdiffl  10427  modqmulnn  10434  modqvalp1  10435  modqmuladdnn0  10460  qnegmod  10461  addmodid  10464  modfzo0difsn  10487  addmodlteq  10490  qexpclz  10652  expgt1  10669  expp1zap  10680  expm1ap  10681  expubnd  10688  bernneq2  10753  expnlbnd  10756  mulsubdivbinom2ap  10803  omgadd  10894  hashun  10897  fihashssdif  10910  hashdifpr  10912  fimaxq  10919  shftuz  10982  mulreap  11029  redivap  11039  imdivap  11046  resqrtcl  11194  xrmaxltsup  11423  xrmaxaddlem  11425  xrmaxadd  11426  xrlemininf  11436  xrminltinf  11437  climuni  11458  addcn2  11475  mulcn2  11477  efsub  11846  sin02gt0  11929  cos12dec  11933  dvdsval2  11955  addmodlteqALT  12024  modremain  12094  fldivndvdslt  12102  mulgcdr  12185  gcddiv  12186  rpmulgcd  12193  rplpwr  12194  rppwr  12195  nnminle  12202  qredeq  12264  divgcdcoprmex  12270  cncongr1  12271  cncongr2  12272  dvdsnprmd  12293  euclemma  12314  prmexpb  12319  qnumdenbi  12360  eulerth  12401  fermltl  12402  prmdiv  12403  hashgcdlem  12406  odzcllem  12411  vfermltl  12420  reumodprminv  12422  modprm0  12423  modprmn0modprm0  12425  coprimeprodsq  12426  pythagtriplem1  12434  pythagtriplem3  12436  pythagtriplem4  12437  pythagtriplem10  12438  pythagtriplem6  12439  pythagtriplem7  12440  pythagtriplem8  12441  pythagtriplem9  12442  pythagtriplem11  12443  pythagtriplem12  12444  pythagtriplem13  12445  pythagtriplem14  12446  pythagtriplem15  12447  pythagtriplem16  12448  pythagtriplem17  12449  pythagtriplem19  12451  pythagtrip  12452  pcpremul  12462  pcdvdsb  12489  dvdsprmpweqnn  12505  dvdsprmpweqle  12506  difsqpwdvds  12507  pcfaclem  12518  pcbc  12520  4sqlem12  12571  unennn  12614  nninfdc  12670  setsex  12710  f1ocpbllem  12953  imasaddfnlemg  12957  imasaddvallemg  12958  ercpbl  12974  erlecpbl  12975  qusaddvallemg  12976  fvprif  12986  xpsfrnel2  12989  plusfvalg  13006  insubm  13117  grpidrcan  13197  grpidlcan  13198  grpsubpropd2  13237  imasgrp2  13240  imasgrp  13241  mulgnnsubcl  13264  mulgnn0subcl  13265  mulgsubcl  13266  mulgaddcom  13276  mulginvcom  13277  mulgnnass  13287  mulgassr  13290  mulgpropdg  13294  submmulg  13296  subgcl  13314  subgsubcl  13315  subgsub  13316  subgmulg  13318  nsgconj  13336  ghmsub  13381  ghmrn  13387  ghmeqker  13401  f1ghm0to0  13402  ablinvadd  13440  ablsub4  13443  abladdsub4  13444  subcmnd  13463  imasabl  13466  rngcl  13500  imasrng  13512  srgcl  13526  srg1zr  13543  srgen1zr  13544  ringcl  13569  crngcom  13570  ringidss  13585  mulgass2  13614  imasring  13620  opprmulg  13627  unitmulclb  13670  unitdvcl  13692  rhmmul  13720  rhmdvdsr  13731  subrngmcl  13765  subrgmcl  13789  subrgdv  13794  subrgugrp  13796  domneq0  13828  scafvalg  13863  lmodprop2d  13904  lssclg  13920  lssvnegcl  13932  lssintclm  13940  sralmod  14006  rnglidlmcl  14036  lidlnegcl  14041  rspssp  14050  rnglidlmsgrp  14053  rnglidlrng  14054  2idlcpblrng  14079  qus2idrng  14081  zndvds  14205  znleval2  14210  basgen  14316  2basgeng  14318  iuncld  14351  neipsm  14390  opnneissb  14391  opnssneib  14392  iscnp3  14439  cnprcl2k  14442  cnpnei  14455  cncnp2m  14467  cnptoprest  14475  sslm  14483  upxp  14508  cnmpt22  14530  distspace  14571  0met  14620  blvalps  14624  blval  14625  ssblps  14661  ssbl  14662  blpnfctr  14675  blopn  14726  blnei  14728  bdxmet  14737  bdbl  14739  metcnp3  14747  tgqioo  14791  ptolemy  15060  sinq12gt0  15066  sincosq1eq  15075  rpcxpadd  15141  cxpmul  15148  rplogbval  15181  logbleb  15197  logbgcd1irr  15203  logbprmirr  15208  lgsfvalg  15246  lgsneg1  15266  lgssq  15281  lgsdinn0  15289  gausslemma2dlem1a  15299  2lgs  15345  2lgsoddprmlem2  15347  bdfind  15592  1dom1el  15637