Theorem 3ad2ant1 1042

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

Syntax hints:   -> wi 4   /\ w3a 1002

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 1004

This theorem is referenced by:  simp1l  1045  simp1r  1046  simp11  1051  simp12  1052  simp13  1053  simp1ll  1084  simp1lr  1085  simp1rl  1086  simp1rr  1087  simp1l1  1114  simp1l2  1115  simp1l3  1116  simp1r1  1117  simp1r2  1118  simp1r3  1119  simp11l  1132  simp11r  1133  simp12l  1134  simp12r  1135  simp13l  1136  simp13r  1137  simp111  1150  simp112  1151  simp113  1152  simp121  1153  simp122  1154  simp123  1155  simp131  1156  simp132  1157  simp133  1158  3anim123i  1208  3jaao  1342  ceqsalt  2826  sbciegft  3059  reupick2  3490  ifbothdc  3637  frirrg  4441  breldmg  4929  fntpg  5377  funimaexglem  5404  fex2  5494  fvun1  5702  fprg  5826  fsnunfv  5844  fnfvima  5878  cocan1  5917  cocan2  5918  mpoeq3dv  6076  fovcld  6115  fvmpopr2d  6147  funexw  6263  mpofvex  6357  poxp  6384  smoiso  6454  tfrlem5  6466  tfrlemibxssdm  6479  tfr1onlembfn  6496  tfri1dALT  6503  tfrcllembfn  6509  rdgon  6538  freccllem  6554  nnawordex  6683  mapxpen  7017  fidceq  7039  fidifsnen  7040  dif1en  7049  en2eqpr  7080  unsnfi  7092  unsnfidcex  7093  unsnfidcel  7094  fisseneq  7107  ordiso2  7213  updjud  7260  mkvprop  7336  endjudisj  7403  xpdjuen  7411  mulcanenq0ec  7643  prltlu  7685  prarloclem3step  7694  prarloclem5  7698  ltasrg  7968  cnegexlem1  8332  addcan  8337  apcotr  8765  apadd1  8766  mulext1  8770  divdivap1  8881  divdivap2  8882  div2negap  8893  divneg2ap  8894  ltmulgt11  9022  ltdiv2  9045  squeeze0  9062  nndivtr  9163  nn0n0n1ge2  9528  zdivmul  9548  gtndiv  9553  eluzuzle  9742  eluzp1p1  9760  qdivcl  9850  irrmul  9854  rpgecl  9890  xaddass  10077  xltadd1  10084  xlt2add  10088  lbico1  10138  lbicc2  10192  zltaddlt1le  10215  uzsubsubfz  10255  elfz1b  10298  elfz0ubfz0  10333  fz0fzelfz0  10335  difelfzle  10342  difelfznle  10343  2ffzeq  10349  fzo1fzo0n0  10395  ubmelfzo  10418  fzonn0p1p1  10431  elfzom1p1elfzo  10432  elfzonelfzo  10448  subfzo0  10460  ceiqle  10547  ceilqle  10548  modqval  10558  flqpmodeq  10561  modq0  10563  negqmod0  10565  modqge0  10566  modqlt  10567  modqdiffl  10569  modqmulnn  10576  modqvalp1  10577  modqmuladdnn0  10602  qnegmod  10603  addmodid  10606  modfzo0difsn  10629  addmodlteq  10632  qexpclz  10794  expgt1  10811  expp1zap  10822  expm1ap  10823  expubnd  10830  bernneq2  10895  expnlbnd  10898  mulsubdivbinom2ap  10945  omgadd  11036  hashun  11039  fihashssdif  11053  hashdifpr  11055  fimaxq  11062  ccatval2  11146  ccatval3  11147  ccatval1lsw  11152  ccatval21sw  11153  ccatass  11156  ccats1val2  11187  fzowrddc  11195  swrdval  11196  swrdclg  11198  swrdval2  11199  swrdnd  11207  swrdlen2  11210  swrdfv2  11211  ccatswrd  11218  pfxn0  11236  pfxsuff1eqwrdeq  11247  swrdswrdlem  11252  ccats1pfxeq  11262  ccats1pfxeqrex  11263  ccatopth2  11265  wrd2ind  11271  pfxccatin12lem3  11280  pfxccat3  11282  swrdccat  11283  pfxccatpfx2  11285  pfxccat3a  11286  swrdccat3b  11288  pfxccatid  11289  ccats1pfxeqbi  11290  shftuz  11344  mulreap  11391  redivap  11401  imdivap  11408  resqrtcl  11556  xrmaxltsup  11785  xrmaxaddlem  11787  xrmaxadd  11788  xrlemininf  11798  xrminltinf  11799  climuni  11820  addcn2  11837  mulcn2  11839  efsub  12208  sin02gt0  12291  cos12dec  12295  dvdsval2  12317  addmodlteqALT  12386  modremain  12456  fldivndvdslt  12464  mulgcdr  12555  gcddiv  12556  rpmulgcd  12563  rplpwr  12564  rppwr  12565  nnminle  12572  qredeq  12634  divgcdcoprmex  12640  cncongr1  12641  cncongr2  12642  dvdsnprmd  12663  euclemma  12684  prmexpb  12689  qnumdenbi  12730  eulerth  12771  fermltl  12772  prmdiv  12773  hashgcdlem  12776  odzcllem  12781  vfermltl  12790  reumodprminv  12792  modprm0  12793  modprmn0modprm0  12795  coprimeprodsq  12796  pythagtriplem1  12804  pythagtriplem3  12806  pythagtriplem4  12807  pythagtriplem10  12808  pythagtriplem6  12809  pythagtriplem7  12810  pythagtriplem8  12811  pythagtriplem9  12812  pythagtriplem11  12813  pythagtriplem12  12814  pythagtriplem13  12815  pythagtriplem14  12816  pythagtriplem15  12817  pythagtriplem16  12818  pythagtriplem17  12819  pythagtriplem19  12821  pythagtrip  12822  pcpremul  12832  pcdvdsb  12859  dvdsprmpweqnn  12875  dvdsprmpweqle  12876  difsqpwdvds  12877  pcfaclem  12888  pcbc  12890  4sqlem12  12941  unennn  12984  nninfdc  13040  setsex  13080  f1ocpbllem  13359  imasaddfnlemg  13363  imasaddvallemg  13364  ercpbl  13380  erlecpbl  13381  qusaddvallemg  13382  fvprif  13392  xpsfrnel2  13395  plusfvalg  13412  imasmnd  13502  insubm  13534  grpidrcan  13614  grpidlcan  13615  grpsubpropd2  13654  pwsinvg  13661  imasgrp2  13663  imasgrp  13664  mulgnnsubcl  13687  mulgnn0subcl  13688  mulgsubcl  13689  mulgaddcom  13699  mulginvcom  13700  mulgnnass  13710  mulgassr  13713  mulgpropdg  13717  submmulg  13719  subgcl  13737  subgsubcl  13738  subgsub  13739  subgmulg  13741  nsgconj  13759  ghmsub  13804  ghmrn  13810  ghmeqker  13824  f1ghm0to0  13825  ablinvadd  13863  ablsub4  13866  abladdsub4  13867  subcmnd  13886  imasabl  13889  rngcl  13923  imasrng  13935  srgcl  13949  srg1zr  13966  srgen1zr  13967  ringcl  13992  crngcom  13993  ringidss  14008  mulgass2  14037  imasring  14043  opprmulg  14050  unitmulclb  14094  unitdvcl  14116  rhmmul  14144  rhmdvdsr  14155  subrngmcl  14189  subrgmcl  14213  subrgdv  14218  subrgugrp  14220  domneq0  14252  scafvalg  14287  lmodprop2d  14328  lssclg  14344  lssvnegcl  14356  lssintclm  14364  sralmod  14430  rnglidlmcl  14460  lidlnegcl  14465  rspssp  14474  rnglidlmsgrp  14477  rnglidlrng  14478  2idlcpblrng  14503  qus2idrng  14505  zndvds  14629  znleval2  14634  basgen  14770  2basgeng  14772  iuncld  14805  neipsm  14844  opnneissb  14845  opnssneib  14846  iscnp3  14893  cnprcl2k  14896  cnpnei  14909  cncnp2m  14921  cnptoprest  14929  sslm  14937  upxp  14962  cnmpt22  14984  distspace  15025  0met  15074  blvalps  15078  blval  15079  ssblps  15115  ssbl  15116  blpnfctr  15129  blopn  15180  blnei  15182  bdxmet  15191  bdbl  15193  metcnp3  15201  tgqioo  15245  ptolemy  15514  sinq12gt0  15520  sincosq1eq  15529  rpcxpadd  15595  cxpmul  15602  rplogbval  15635  logbleb  15651  logbgcd1irr  15657  logbprmirr  15662  lgsfvalg  15700  lgsneg1  15720  lgssq  15735  lgsdinn0  15743  gausslemma2dlem1a  15753  2lgs  15799  2lgsoddprmlem2  15801  funvtxdm2domval  15846  funiedgdm2domval  15847  iedgedgg  15877  lpvtx  15895  incistruhgr  15906  ausgrumgrien  15984  ausgrusgrien  15985  umgr2edgneu  16026  ushgredgedg  16040  ushgredgedgloop  16042  iswlk  16069  wlkl1loop  16104  uspgr2wlkeq  16111  istrl  16129  clwwlkccatlem  16143  clwwlkccat  16144  clwwlknccat  16165  bdfind  16392  1dom1el  16437