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  3450  ifbothdc  3595  frirrg  4386  breldmg  4873  fntpg  5315  funimaexglem  5342  fex2  5429  fvun1  5630  fprg  5748  fsnunfv  5766  fnfvima  5800  cocan1  5837  cocan2  5838  mpoeq3dv  5992  fovcld  6031  fvmpopr2d  6063  funexw  6178  mpofvex  6272  poxp  6299  smoiso  6369  tfrlem5  6381  tfrlemibxssdm  6394  tfr1onlembfn  6411  tfri1dALT  6418  tfrcllembfn  6424  rdgon  6453  freccllem  6469  nnawordex  6596  mapxpen  6918  fidceq  6939  fidifsnen  6940  dif1en  6949  en2eqpr  6977  unsnfi  6989  unsnfidcex  6990  unsnfidcel  6991  fisseneq  7004  ordiso2  7110  updjud  7157  mkvprop  7233  endjudisj  7293  xpdjuen  7301  mulcanenq0ec  7529  prltlu  7571  prarloclem3step  7580  prarloclem5  7584  ltasrg  7854  cnegexlem1  8218  addcan  8223  apcotr  8651  apadd1  8652  mulext1  8656  divdivap1  8767  divdivap2  8768  div2negap  8779  divneg2ap  8780  ltmulgt11  8908  ltdiv2  8931  squeeze0  8948  nndivtr  9049  nn0n0n1ge2  9413  zdivmul  9433  gtndiv  9438  eluzuzle  9626  eluzp1p1  9644  qdivcl  9734  irrmul  9738  rpgecl  9774  xaddass  9961  xltadd1  9968  xlt2add  9972  lbico1  10022  lbicc2  10076  zltaddlt1le  10099  uzsubsubfz  10139  elfz1b  10182  elfz0ubfz0  10217  fz0fzelfz0  10219  difelfzle  10226  difelfznle  10227  2ffzeq  10233  fzo1fzo0n0  10276  ubmelfzo  10293  fzonn0p1p1  10306  elfzom1p1elfzo  10307  elfzonelfzo  10323  subfzo0  10335  ceiqle  10422  ceilqle  10423  modqval  10433  flqpmodeq  10436  modq0  10438  negqmod0  10440  modqge0  10441  modqlt  10442  modqdiffl  10444  modqmulnn  10451  modqvalp1  10452  modqmuladdnn0  10477  qnegmod  10478  addmodid  10481  modfzo0difsn  10504  addmodlteq  10507  qexpclz  10669  expgt1  10686  expp1zap  10697  expm1ap  10698  expubnd  10705  bernneq2  10770  expnlbnd  10773  mulsubdivbinom2ap  10820  omgadd  10911  hashun  10914  fihashssdif  10927  hashdifpr  10929  fimaxq  10936  shftuz  10999  mulreap  11046  redivap  11056  imdivap  11063  resqrtcl  11211  xrmaxltsup  11440  xrmaxaddlem  11442  xrmaxadd  11443  xrlemininf  11453  xrminltinf  11454  climuni  11475  addcn2  11492  mulcn2  11494  efsub  11863  sin02gt0  11946  cos12dec  11950  dvdsval2  11972  addmodlteqALT  12041  modremain  12111  fldivndvdslt  12119  mulgcdr  12210  gcddiv  12211  rpmulgcd  12218  rplpwr  12219  rppwr  12220  nnminle  12227  qredeq  12289  divgcdcoprmex  12295  cncongr1  12296  cncongr2  12297  dvdsnprmd  12318  euclemma  12339  prmexpb  12344  qnumdenbi  12385  eulerth  12426  fermltl  12427  prmdiv  12428  hashgcdlem  12431  odzcllem  12436  vfermltl  12445  reumodprminv  12447  modprm0  12448  modprmn0modprm0  12450  coprimeprodsq  12451  pythagtriplem1  12459  pythagtriplem3  12461  pythagtriplem4  12462  pythagtriplem10  12463  pythagtriplem6  12464  pythagtriplem7  12465  pythagtriplem8  12466  pythagtriplem9  12467  pythagtriplem11  12468  pythagtriplem12  12469  pythagtriplem13  12470  pythagtriplem14  12471  pythagtriplem15  12472  pythagtriplem16  12473  pythagtriplem17  12474  pythagtriplem19  12476  pythagtrip  12477  pcpremul  12487  pcdvdsb  12514  dvdsprmpweqnn  12530  dvdsprmpweqle  12531  difsqpwdvds  12532  pcfaclem  12543  pcbc  12545  4sqlem12  12596  unennn  12639  nninfdc  12695  setsex  12735  f1ocpbllem  13012  imasaddfnlemg  13016  imasaddvallemg  13017  ercpbl  13033  erlecpbl  13034  qusaddvallemg  13035  fvprif  13045  xpsfrnel2  13048  plusfvalg  13065  imasmnd  13155  insubm  13187  grpidrcan  13267  grpidlcan  13268  grpsubpropd2  13307  pwsinvg  13314  imasgrp2  13316  imasgrp  13317  mulgnnsubcl  13340  mulgnn0subcl  13341  mulgsubcl  13342  mulgaddcom  13352  mulginvcom  13353  mulgnnass  13363  mulgassr  13366  mulgpropdg  13370  submmulg  13372  subgcl  13390  subgsubcl  13391  subgsub  13392  subgmulg  13394  nsgconj  13412  ghmsub  13457  ghmrn  13463  ghmeqker  13477  f1ghm0to0  13478  ablinvadd  13516  ablsub4  13519  abladdsub4  13520  subcmnd  13539  imasabl  13542  rngcl  13576  imasrng  13588  srgcl  13602  srg1zr  13619  srgen1zr  13620  ringcl  13645  crngcom  13646  ringidss  13661  mulgass2  13690  imasring  13696  opprmulg  13703  unitmulclb  13746  unitdvcl  13768  rhmmul  13796  rhmdvdsr  13807  subrngmcl  13841  subrgmcl  13865  subrgdv  13870  subrgugrp  13872  domneq0  13904  scafvalg  13939  lmodprop2d  13980  lssclg  13996  lssvnegcl  14008  lssintclm  14016  sralmod  14082  rnglidlmcl  14112  lidlnegcl  14117  rspssp  14126  rnglidlmsgrp  14129  rnglidlrng  14130  2idlcpblrng  14155  qus2idrng  14157  zndvds  14281  znleval2  14286  basgen  14400  2basgeng  14402  iuncld  14435  neipsm  14474  opnneissb  14475  opnssneib  14476  iscnp3  14523  cnprcl2k  14526  cnpnei  14539  cncnp2m  14551  cnptoprest  14559  sslm  14567  upxp  14592  cnmpt22  14614  distspace  14655  0met  14704  blvalps  14708  blval  14709  ssblps  14745  ssbl  14746  blpnfctr  14759  blopn  14810  blnei  14812  bdxmet  14821  bdbl  14823  metcnp3  14831  tgqioo  14875  ptolemy  15144  sinq12gt0  15150  sincosq1eq  15159  rpcxpadd  15225  cxpmul  15232  rplogbval  15265  logbleb  15281  logbgcd1irr  15287  logbprmirr  15292  lgsfvalg  15330  lgsneg1  15350  lgssq  15365  lgsdinn0  15373  gausslemma2dlem1a  15383  2lgs  15429  2lgsoddprmlem2  15431  bdfind  15676  1dom1el  15721