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  2803  sbciegft  3036  reupick2  3467  ifbothdc  3614  frirrg  4415  breldmg  4903  fntpg  5349  funimaexglem  5376  fex2  5464  fvun1  5668  fprg  5790  fsnunfv  5808  fnfvima  5842  cocan1  5879  cocan2  5880  mpoeq3dv  6034  fovcld  6073  fvmpopr2d  6105  funexw  6220  mpofvex  6314  poxp  6341  smoiso  6411  tfrlem5  6423  tfrlemibxssdm  6436  tfr1onlembfn  6453  tfri1dALT  6460  tfrcllembfn  6466  rdgon  6495  freccllem  6511  nnawordex  6638  mapxpen  6970  fidceq  6992  fidifsnen  6993  dif1en  7002  en2eqpr  7030  unsnfi  7042  unsnfidcex  7043  unsnfidcel  7044  fisseneq  7057  ordiso2  7163  updjud  7210  mkvprop  7286  endjudisj  7353  xpdjuen  7361  mulcanenq0ec  7593  prltlu  7635  prarloclem3step  7644  prarloclem5  7648  ltasrg  7918  cnegexlem1  8282  addcan  8287  apcotr  8715  apadd1  8716  mulext1  8720  divdivap1  8831  divdivap2  8832  div2negap  8843  divneg2ap  8844  ltmulgt11  8972  ltdiv2  8995  squeeze0  9012  nndivtr  9113  nn0n0n1ge2  9478  zdivmul  9498  gtndiv  9503  eluzuzle  9691  eluzp1p1  9709  qdivcl  9799  irrmul  9803  rpgecl  9839  xaddass  10026  xltadd1  10033  xlt2add  10037  lbico1  10087  lbicc2  10141  zltaddlt1le  10164  uzsubsubfz  10204  elfz1b  10247  elfz0ubfz0  10282  fz0fzelfz0  10284  difelfzle  10291  difelfznle  10292  2ffzeq  10298  fzo1fzo0n0  10344  ubmelfzo  10366  fzonn0p1p1  10379  elfzom1p1elfzo  10380  elfzonelfzo  10396  subfzo0  10408  ceiqle  10495  ceilqle  10496  modqval  10506  flqpmodeq  10509  modq0  10511  negqmod0  10513  modqge0  10514  modqlt  10515  modqdiffl  10517  modqmulnn  10524  modqvalp1  10525  modqmuladdnn0  10550  qnegmod  10551  addmodid  10554  modfzo0difsn  10577  addmodlteq  10580  qexpclz  10742  expgt1  10759  expp1zap  10770  expm1ap  10771  expubnd  10778  bernneq2  10843  expnlbnd  10846  mulsubdivbinom2ap  10893  omgadd  10984  hashun  10987  fihashssdif  11000  hashdifpr  11002  fimaxq  11009  ccatval2  11092  ccatval3  11093  ccatval1lsw  11098  ccatval21sw  11099  ccatass  11102  ccats1val2  11130  fzowrddc  11138  swrdval  11139  swrdclg  11141  swrdval2  11142  swrdnd  11150  swrdlen2  11153  swrdfv2  11154  ccatswrd  11161  pfxn0  11179  pfxsuff1eqwrdeq  11190  swrdswrdlem  11195  ccats1pfxeq  11205  ccats1pfxeqrex  11206  ccatopth2  11208  wrd2ind  11214  pfxccatin12lem3  11223  pfxccat3  11225  swrdccat  11226  pfxccatpfx2  11228  pfxccat3a  11229  swrdccat3b  11231  pfxccatid  11232  ccats1pfxeqbi  11233  shftuz  11243  mulreap  11290  redivap  11300  imdivap  11307  resqrtcl  11455  xrmaxltsup  11684  xrmaxaddlem  11686  xrmaxadd  11687  xrlemininf  11697  xrminltinf  11698  climuni  11719  addcn2  11736  mulcn2  11738  efsub  12107  sin02gt0  12190  cos12dec  12194  dvdsval2  12216  addmodlteqALT  12285  modremain  12355  fldivndvdslt  12363  mulgcdr  12454  gcddiv  12455  rpmulgcd  12462  rplpwr  12463  rppwr  12464  nnminle  12471  qredeq  12533  divgcdcoprmex  12539  cncongr1  12540  cncongr2  12541  dvdsnprmd  12562  euclemma  12583  prmexpb  12588  qnumdenbi  12629  eulerth  12670  fermltl  12671  prmdiv  12672  hashgcdlem  12675  odzcllem  12680  vfermltl  12689  reumodprminv  12691  modprm0  12692  modprmn0modprm0  12694  coprimeprodsq  12695  pythagtriplem1  12703  pythagtriplem3  12705  pythagtriplem4  12706  pythagtriplem10  12707  pythagtriplem6  12708  pythagtriplem7  12709  pythagtriplem8  12710  pythagtriplem9  12711  pythagtriplem11  12712  pythagtriplem12  12713  pythagtriplem13  12714  pythagtriplem14  12715  pythagtriplem15  12716  pythagtriplem16  12717  pythagtriplem17  12718  pythagtriplem19  12720  pythagtrip  12721  pcpremul  12731  pcdvdsb  12758  dvdsprmpweqnn  12774  dvdsprmpweqle  12775  difsqpwdvds  12776  pcfaclem  12787  pcbc  12789  4sqlem12  12840  unennn  12883  nninfdc  12939  setsex  12979  f1ocpbllem  13257  imasaddfnlemg  13261  imasaddvallemg  13262  ercpbl  13278  erlecpbl  13279  qusaddvallemg  13280  fvprif  13290  xpsfrnel2  13293  plusfvalg  13310  imasmnd  13400  insubm  13432  grpidrcan  13512  grpidlcan  13513  grpsubpropd2  13552  pwsinvg  13559  imasgrp2  13561  imasgrp  13562  mulgnnsubcl  13585  mulgnn0subcl  13586  mulgsubcl  13587  mulgaddcom  13597  mulginvcom  13598  mulgnnass  13608  mulgassr  13611  mulgpropdg  13615  submmulg  13617  subgcl  13635  subgsubcl  13636  subgsub  13637  subgmulg  13639  nsgconj  13657  ghmsub  13702  ghmrn  13708  ghmeqker  13722  f1ghm0to0  13723  ablinvadd  13761  ablsub4  13764  abladdsub4  13765  subcmnd  13784  imasabl  13787  rngcl  13821  imasrng  13833  srgcl  13847  srg1zr  13864  srgen1zr  13865  ringcl  13890  crngcom  13891  ringidss  13906  mulgass2  13935  imasring  13941  opprmulg  13948  unitmulclb  13991  unitdvcl  14013  rhmmul  14041  rhmdvdsr  14052  subrngmcl  14086  subrgmcl  14110  subrgdv  14115  subrgugrp  14117  domneq0  14149  scafvalg  14184  lmodprop2d  14225  lssclg  14241  lssvnegcl  14253  lssintclm  14261  sralmod  14327  rnglidlmcl  14357  lidlnegcl  14362  rspssp  14371  rnglidlmsgrp  14374  rnglidlrng  14375  2idlcpblrng  14400  qus2idrng  14402  zndvds  14526  znleval2  14531  basgen  14667  2basgeng  14669  iuncld  14702  neipsm  14741  opnneissb  14742  opnssneib  14743  iscnp3  14790  cnprcl2k  14793  cnpnei  14806  cncnp2m  14818  cnptoprest  14826  sslm  14834  upxp  14859  cnmpt22  14881  distspace  14922  0met  14971  blvalps  14975  blval  14976  ssblps  15012  ssbl  15013  blpnfctr  15026  blopn  15077  blnei  15079  bdxmet  15088  bdbl  15090  metcnp3  15098  tgqioo  15142  ptolemy  15411  sinq12gt0  15417  sincosq1eq  15426  rpcxpadd  15492  cxpmul  15499  rplogbval  15532  logbleb  15548  logbgcd1irr  15554  logbprmirr  15559  lgsfvalg  15597  lgsneg1  15617  lgssq  15632  lgsdinn0  15640  gausslemma2dlem1a  15650  2lgs  15696  2lgsoddprmlem2  15698  funvtxdm2domval  15743  funiedgdm2domval  15744  iedgedgg  15772  lpvtx  15790  incistruhgr  15801  bdfind  16081  1dom1el  16126