MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  adantllr Structured version   Visualization version   GIF version

Theorem adantllr 750
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
Hypothesis
Ref Expression
adantl2.1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Assertion
Ref Expression
adantllr ((((𝜑𝜏) ∧ 𝜓) ∧ 𝜒) → 𝜃)

Proof of Theorem adantllr
StepHypRef Expression
1 simpl 471 . 2 ((𝜑𝜏) → 𝜑)
2 adantl2.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylanl1 679 1 ((((𝜑𝜏) ∧ 𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 195  df-an 384
This theorem is referenced by:  adantl3r  781  r19.29an  3054  elsnxpOLD  5577  oewordri  7532  marypha1lem  8195  gruwun  9487  lemul12b  10725  rlimsqzlem  14169  fsumrlim  14326  fsumo1  14327  lcmdvds  15101  isacs2  16079  dfgrp3lem  17278  tgcl  20522  neindisj  20669  neiptoptop  20683  isr0  21288  cnextcn  21619  ustuqtop4  21796  metss  22060  mbfsup  23150  itg2i1fseqle  23240  ditgsplit  23344  itgulm  23879  leibpi  24382  dchrisumlem3  24893  iscgrglt  25123  legov  25194  legov2  25195  legtrid  25200  colopp  25375  f1otrg  25465  cusgrasize2inds  25767  grpoidinvlem3  26506  grpoideu  26509  grporcan  26518  blocni  26846  normcan  27621  unoplin  27965  hmoplin  27987  nmophmi  28076  mdslmd3i  28377  chirredlem1  28435  chirredlem2  28436  mdsymlem5  28452  cdj1i  28478  fpwrelmap  28698  archiabllem1  28880  archiabl  28885  isarchiofld  28950  locfinreflem  29037  pstmxmet  29070  ordtconlem1  29100  esumcvg  29277  esum2d  29284  esumiun  29285  ldgenpisyslem1  29355  omssubadd  29491  signstfvneq0  29777  elicc3  31283  knoppcnlem9  31463  lindsenlbs  32373  matunitlindflem1  32374  poimirlem17  32395  poimirlem20  32398  poimirlem27  32405  poimirlem29  32407  poimir  32411  heicant  32413  itg2addnclem  32430  ftc1anclem5  32458  ftc1anclem6  32459  ftc1anclem7  32460  ftc1anclem8  32461  ftc1anc  32462  fzmul  32506  fdc  32510  fdc1  32511  incsequz2  32514  rrncmslem  32600  ghomco  32659  rngoisocnv  32749  ispridlc  32838  cvgdvgrat  37333  binomcxplemnotnn0  37376  founiiun0  38171  supxrge  38295  suplesup  38296  lptre2pt  38507  0ellimcdiv  38516  limclner  38518  icccncfext  38573  cncfiooiccre  38581  fperdvper  38608  dvnprodlem2  38637  iblcncfioo  38670  stoweidlem35  38728  wallispilem3  38760  fourierdlem20  38820  fourierdlem34  38834  fourierdlem39  38839  fourierdlem42  38842  fourierdlem46  38845  fourierdlem48  38847  fourierdlem49  38848  fourierdlem63  38862  fourierdlem64  38863  fourierdlem73  38872  fourierdlem87  38886  fourierdlem97  38896  fourierdlem103  38902  fourierdlem104  38903  fourierdlem111  38910  etransclem32  38959  etransclem33  38960  etransclem35  38962  sge0cl  39074  sge0f1o  39075  sge0split  39102  sge0iunmptlemre  39108  sge0rpcpnf  39114  sge0xadd  39128  nnfoctbdjlem  39148  ismeannd  39160  omeiunltfirp  39209  hoidmvlelem3  39287  hoidmvle  39290  ovncvr2  39301  hspdifhsp  39306  hspmbllem2  39317  ovnsubadd2lem  39335  pimdecfgtioo  39404  pimincfltioo  39405  smflimlem1  39457  cusgrsize2inds  40667  aacllem  42315
  Copyright terms: Public domain W3C validator