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

Theorem adantllr 754
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 473 . 2 ((𝜑𝜏) → 𝜑)
2 adantl2.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylanl1 681 1 ((((𝜑𝜏) ∧ 𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 386
This theorem is referenced by:  adantl3r  785  r19.29an  3072  elsnxpOLD  5647  oewordri  7632  marypha1lem  8299  gruwun  9595  lemul12b  10840  rlimsqzlem  14329  fsumrlim  14489  fsumo1  14490  lcmdvds  15264  isacs2  16254  dfgrp3lem  17453  tgcl  20713  neindisj  20861  neiptoptop  20875  isr0  21480  cnextcn  21811  ustuqtop4  21988  metss  22253  mbfsup  23371  itg2i1fseqle  23461  ditgsplit  23565  itgulm  24100  leibpi  24603  dchrisumlem3  25114  iscgrglt  25343  legov  25414  legov2  25415  legtrid  25420  colopp  25595  f1otrg  25685  cusgrsize2inds  26270  grpoidinvlem3  27248  grpoideu  27251  grporcan  27260  blocni  27548  normcan  28323  unoplin  28667  hmoplin  28689  nmophmi  28778  mdslmd3i  29079  chirredlem1  29137  chirredlem2  29138  mdsymlem5  29154  cdj1i  29180  fpwrelmap  29392  archiabllem1  29574  archiabl  29579  isarchiofld  29644  locfinreflem  29731  pstmxmet  29764  ordtconnlem1  29794  esumcvg  29971  esum2d  29978  esumiun  29979  ldgenpisyslem1  30049  omssubadd  30185  signstfvneq0  30471  elicc3  32006  knoppcnlem9  32186  lindsenlbs  33075  matunitlindflem1  33076  poimirlem17  33097  poimirlem20  33100  poimirlem27  33107  poimirlem29  33109  poimir  33113  heicant  33115  itg2addnclem  33132  ftc1anclem5  33160  ftc1anclem6  33161  ftc1anclem7  33162  ftc1anclem8  33163  ftc1anc  33164  fzmul  33208  fdc  33212  fdc1  33213  incsequz2  33216  rrncmslem  33302  ghomco  33361  rngoisocnv  33451  ispridlc  33540  cvgdvgrat  38033  binomcxplemnotnn0  38076  founiiun0  38886  supxrge  39053  suplesup  39054  supxrunb3  39122  lptre2pt  39308  0ellimcdiv  39317  limclner  39319  limsuppnfdlem  39369  limsuppnflem  39378  limsupmnflem  39388  icccncfext  39435  cncfiooiccre  39443  fperdvper  39470  dvnprodlem2  39499  iblcncfioo  39531  stoweidlem35  39589  wallispilem3  39621  fourierdlem20  39681  fourierdlem34  39695  fourierdlem39  39700  fourierdlem42  39703  fourierdlem46  39706  fourierdlem48  39708  fourierdlem49  39709  fourierdlem63  39723  fourierdlem64  39724  fourierdlem73  39733  fourierdlem87  39747  fourierdlem97  39757  fourierdlem103  39763  fourierdlem104  39764  fourierdlem111  39771  etransclem32  39820  etransclem33  39821  etransclem35  39823  sge0cl  39935  sge0f1o  39936  sge0split  39963  sge0iunmptlemre  39969  sge0rpcpnf  39975  sge0xadd  39989  nnfoctbdjlem  40009  ismeannd  40021  omeiunltfirp  40070  hoidmvlelem3  40148  hoidmvle  40151  ovncvr2  40162  hspdifhsp  40167  hspmbllem2  40178  ovnsubadd2lem  40196  pimdecfgtioo  40264  pimincfltioo  40265  smflimlem1  40316  smflimmpt  40353  aacllem  41880
  Copyright terms: Public domain W3C validator