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

 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 474 . 2 ((𝜑𝜏) → 𝜑)
2 adantl2.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylanl1 685 1 ((((𝜑𝜏) ∧ 𝜓) ∧ 𝜒) → 𝜃)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383 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 197  df-an 385 This theorem is referenced by:  adantl3r  803  ad4ant134  1182  ad5ant145  1471  r19.29an  3215  elsnxpOLD  5839  oewordri  7841  marypha1lem  8504  gruwun  9827  lemul12b  11072  rlimsqzlem  14578  fsumrlim  14742  fsumo1  14743  lcmdvds  15523  isacs2  16515  dfgrp3lem  17714  tgcl  20975  neindisj  21123  neiptoptop  21137  isr0  21742  cnextcn  22072  ustuqtop4  22249  metss  22514  mbfsup  23630  itg2i1fseqle  23720  ditgsplit  23824  itgulm  24361  leibpi  24868  dchrisumlem3  25379  iscgrglt  25608  legov  25679  legov2  25680  legtrid  25685  colopp  25860  f1otrg  25950  cusgrsize2inds  26559  grpoidinvlem3  27669  grpoideu  27672  grporcan  27681  blocni  27969  normcan  28744  unoplin  29088  hmoplin  29110  nmophmi  29199  mdslmd3i  29500  chirredlem1  29558  chirredlem2  29559  mdsymlem5  29575  cdj1i  29601  fpwrelmap  29817  fsumiunle  29884  archiabllem1  30056  archiabl  30061  isarchiofld  30126  locfinreflem  30216  pstmxmet  30249  ordtconnlem1  30279  esumcvg  30457  esum2d  30464  esumiun  30465  ldgenpisyslem1  30535  omssubadd  30671  signstfvneq0  30958  circlemeth  31027  elicc3  32617  knoppcnlem9  32797  lindsenlbs  33717  matunitlindflem1  33718  poimirlem17  33739  poimirlem20  33742  poimirlem27  33749  poimirlem29  33751  poimir  33755  heicant  33757  itg2addnclem  33774  ftc1anclem5  33802  ftc1anclem6  33803  ftc1anclem7  33804  ftc1anclem8  33805  ftc1anc  33806  fzmul  33850  fdc  33854  fdc1  33855  incsequz2  33858  rrncmslem  33944  ghomco  34003  rngoisocnv  34093  ispridlc  34182  cvgdvgrat  39014  binomcxplemnotnn0  39057  founiiun0  39876  supxrge  40052  suplesup  40053  supxrunb3  40121  lptre2pt  40375  0ellimcdiv  40384  limclner  40386  limsuppnfdlem  40436  limsuppnflem  40445  limsupmnflem  40455  liminfreuzlem  40537  liminflimsupclim  40542  cnrefiisplem  40558  climxlim2lem  40574  icccncfext  40603  cncfiooiccre  40611  fperdvper  40636  dvnprodlem2  40665  iblcncfioo  40697  stoweidlem35  40755  wallispilem3  40787  fourierdlem20  40847  fourierdlem34  40861  fourierdlem39  40866  fourierdlem42  40869  fourierdlem46  40872  fourierdlem48  40874  fourierdlem49  40875  fourierdlem63  40889  fourierdlem64  40890  fourierdlem73  40899  fourierdlem87  40913  fourierdlem97  40923  fourierdlem103  40929  fourierdlem104  40930  fourierdlem111  40937  etransclem32  40986  etransclem33  40987  etransclem35  40989  sge0cl  41101  sge0f1o  41102  sge0split  41129  sge0iunmptlemre  41135  sge0rpcpnf  41141  sge0xadd  41155  nnfoctbdjlem  41175  ismeannd  41187  omeiunltfirp  41239  hoidmvlelem3  41317  hoidmvle  41320  ovncvr2  41331  hspdifhsp  41336  hspmbllem2  41347  ovnsubadd2lem  41365  pimdecfgtioo  41433  pimincfltioo  41434  smflimlem1  41485  smflimmpt  41522  aacllem  43060
 Copyright terms: Public domain W3C validator