Theorem adantll 428

Description: Deduction adding a conjunct to antecedent.

Hypothesis

Ref	Expression
adant2.1	|- ((ph /\ ps) -> ch)

Assertion

Ref	Expression
adantll	|- (((th /\ ph) /\ ps) -> ch)

Proof of Theorem adantll

Step	Hyp	Ref	Expression
1		adant2.1	. . . 4 |- ((ph /\ ps) -> ch)
2	1	ex 402	. . 3 |- (ph -> (ps -> ch))
3	2	adantl 424	. 2 |- ((th /\ ph) -> (ps -> ch))
4	3	imp 377	1 |- (((th /\ ph) /\ ps) -> ch)

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  ad2ant2l 444  ad2ant2lr 446  3ad2antl3 1040  3adant1l 1090  ax11eq 1754  ax11el 1755  reu6 2443  tz7.7 3684  limsssuc 3934  ssimaex 4729  eqfnfv 4766  dffo4 4793  fopab2 4796  fconst2g 4821  isotr 4874  isotrALT 4875  curry1 5075  curry2 5078  oe0 5206  oesuc 5211  oecl 5218  oeclOLD 5219  oaordi 5227  oawordri 5232  oaass 5243  omordi 5245  omword2 5253  omlimcl 5257  odi 5258  omass 5259  oeoe 5274  nneob 5312  omsmolem 5313  dom2d 5463  ac6sfi 5509  sbthlem9 5518  enen1 5540  sdomen1 5544  sdomen2 5545  riota5 5580  mapenlem2 5584  mapxpen 5589  xpmapenlem3 5592  xpmapenlem4 5593  php3 5609  onomeneq 5612  finsucdom 5620  fiint 5650  fodomfi 5656  fodomfib 5657  supmo 5666  ordiso 5683  ordtypelem6 5689  ordtypelem7 5690  hartog 5693  ac6lem 5916  zorn2lem6 5955  axrepnd 6098  axpowndlem2 6102  axpowndlem4 6104  axinfndlem1 6109  axinfnd 6110  axacndlem4 6114  axacndlem5 6115  axacnd 6116  ltexpq 6232  ltrpq 6237  prcdpq 6249  addclprlem2 6271  prlem934b 6290  ltexpri 6301  prlem936b 6306  ssgt0sr 6369  add4 6491  cnegex 6502  1re 6598  axsup 6676  xrlttr 6728  ltleadd 6829  divadddiv 6960  lt2mul2div 7054  lediv12a 7079  nn2ge 7125  infmrcl 7278  xrsupsslem 7285  xrinfmsslem 7286  supxrunb1 7298  supxrunb2 7299  zextle 7401  modadd1 7518  modmul1 7519  iooin 7539  elioc2 7558  elico2 7559  elicc2 7560  elfz2nn0 7667  fzaddel 7672  fzsuc 7678  fzrev 7689  fzrevral 7698  fsequb2 7703  mulexp 7836  expadd 7839  expmul 7840  expmwordi 7851  expnbnd 7901  sqr2irrlem3 7976  seq1ublem 8163  cau2i 8165  caubndi 8178  fsum1ps 8278  fsumrev 8289  fsumshft 8291  fsumshftm 8292  fsummulc1 8293  fsumdivc 8295  fsumdivcALT 8296  fsum2mul 8297  climshfti 8364  climaddlem3 8376  climaddc2 8379  climmullem4 8383  climmullem5 8384  climmullem8 8387  climsub 8390  climsupi 8415  climcaui 8416  caucvglem5 8421  caucvglem6 8422  caucvgi 8423  cvgcmp3ci 8447  cvgratlem1 8512  fsum0diag4 8523  acdc3lem 8754  acdc2lem1 8757  acdc5lem1 8760  acdclem 8763  unbenlem 8773  infpnlem1 8775  ruclem13 8791  infxpidmlem1 8821  infxpidmlem11 8831  infxpidmlem12 8832  tgss2 8907  txbas 8933  elcls 8980  cnpnei 9043  cnconst 9057  metxp 9111  metcnplem 9164  metcnp2 9166  metcnss 9176  metcnss2 9177  tgioolem 9192  lmconst 9212  lmnn 9213  iscaunns 9222  metcnp4lem2 9247  metcnp4 9248  xplmi 9251  xpcn 9254  bopcnlem2 9260  iscms2lem3 9269  iscms2lem5 9271  bcthlem2 9278  bcthlem26 9302  bcthlem29 9305  grpidinvlem3 9330  grpidinv 9332  grpideu 9333  isgrp2i 9360  ssga 9455  vacnlem5 9671  va1cnlem 9684  sm1cnilem 9686  nmoub3i 9775  nmlno0lem 9793  nmlnoubi 9796  blocnilem 9804  blocni 9805  ipasslem3 9833  ipblnfi 9857  ubthlem5 9876  ubthlem12 9883  ubthlem12OLD 9884  spwpr2 10001  cdrci 10182  fiuni 10219  tx2cn 10224  upxp 10225  txcn 10227  subtopmet 10256  fgfil 10290  cncomp 10331  comptoppr 10332  hvaddsub4 10578  chocunii 10805  occllem6 10811  shsel3 10912  chj4 11091  spansncol 11124  5oalem2 11235  3oalem2 11243  adjsym 11396  cnvadj 11453  nmopub2tALT 11470  unoplin 11481  counop 11482  nmfnleub2 11487  hmoplin 11503  brafnmul 11512  nmlnop0iALT 11557  nmopun 11576  nmcopexlem6 11593  lnopconi 11600  nmcfnexlem6 11622  lnfnconi 11627  nlelchi 11631  riesz3i 11632  riesz1 11635  cnlnadjlem2 11638  cnlnadjlem6 11642  adjmul 11662  adjadd 11663  bra11 11679  cnvbraval 11681  kbass5 11691  kbass6 11692  leop2 11695  leopadd 11703  leopmuli 11704  leoptri 11707  leopnmid 11709  nmopleid 11710  pj3si 11780  hstel2 11791  cvcon3 11856  dmdmd 11872  dmdbr5 11880  mdsl0 11882  mdslmd1lem1 11897  mdslmd1lem2 11898  mdslmd3i 11904  superpos 11926  irredlem2 11963  irredlem3 11964  mdsymlem3 11977  mdsymlem5 11979  mdsymlem6 11980  sumdmdlem 11990  cdjreui 12004  cdj1i 12005  cdj3i 12013  fnn0ind 13611  fseq1cl 13619  gcdcllem3 13720  dfon2lem6 13854  predso 13895  preddowncl 13907  tz6.26 13913  poseq 13954  soseq 13955  axfelem5 14035  axfelem13 14043  toplat 14638  curgrpact 14735  fgsb 14921  fgsb2 14925  supexr 15043  idsubfun 15206  elicc3 15362  fictblem 15370  inficlALT 15372  ordisoOLD 15374  ordtypelem6OLD 15380  ordtypelem7OLD 15381  hartogOLD 15384  subsubtop 15423  compsub 15431  hscptsscld 15434  alexsublem4 15440  connsub 15443  cnconn 15444  conntoppr 15445  reconnlem1 15446  neibastop2lem3 15521  neibastop3 15524  topjoin 15527  fnemeet2 15529  fnejoin1 15530  supfil 15560  filssufil 15571  uffixfr 15575  ufilen 15579  limfilcf 15587  rnelfmlem 15592  fmfnfm 15598  fcluscf 15612  fcluscomplem 15620  filnetlem3 15642  filnetlem5 15644  foco2 15686  eqfnun 15705  upixp 15729  fimax 15746  indexdom 15754  frfi 15771  pofun 15772  filbcmb 15776  fzadd2 15791  sdc 15811  fdc 15812  incsequz 15815  metf1o 15843  blssp 15844  mettrifi2 15848  geomcau 15849  caushft 15851  iccsplit 15854  iccshftr 15857  iccshftl 15859  iccdil 15861  icccntr 15863  icoopnst 15876  lincmb01cmp 15878  lincmb01icc 15879  oprpiece1res2 15881  cnss 15892  tlmconst 15907  txmet 15925  sstotbnd 15936  totbndss 15937  bndss 15942  totbndbnd 15944  ismtycnv 15949  ismtyhmeolem 15950  ismtyhmeo 15951  ismtybndlem 15952  ismtyres 15954  heiborlem16 15970  heiborlem23 15977  heiborlem32 15986  heiborlem34 15988  heiborlem36 15990  rrnmet 16016  rrndstprj1 16017  rrncms 16019  rrntotbndlem1 16020  rrntotbndlem2 16021  rrntotbnd 16022  iccbnd 16026  phtpycolem5 16055  phtpyco 16056  reparpht 16065  pcoval2 16075  pcohtpylem3 16082  pcohtpy 16083  pcoass 16085  isdivrng2 16111  rngisocnv 16135  unichnidl 16179  lubss 16897  grpidinvlem3NEW 17111  grpidinvNEW 17113  grpideuNEW 17114  pmapglb2 17253  pmapglb2x 17254  polval2 17319

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164  df-an 242

Copyright terms: Public domain