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

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

Proof of Theorem adantlll
StepHypRef Expression
1 simpr 479 . 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:  ad4ant234  1181  fun11iun  7283  oewordri  7833  sbthlem8  8234  xmulass  12302  caucvgb  14601  clsnsg  22106  metustto  22551  grpoidinvlem3  27661  nmoub3i  27929  riesz3i  29222  csmdsymi  29494  finxpreclem3  33533  fin2so  33701  matunitlindflem1  33710  mblfinlem2  33752  mblfinlem3  33753  ismblfin  33755  itg2addnclem  33766  ftc1anclem7  33796  ftc1anc  33798  fzmul  33842  fdc  33846  incsequz2  33850  isbnd3  33888  bndss  33890  ismtyres  33912  rngoisocnv  34085  xralrple2  40060  xralrple3  40080  limsupmnflem  40447  climrescn  40475  dirkertrigeq  40813  fourierdlem12  40831  fourierdlem50  40868  fourierdlem103  40921  fourierdlem104  40922  etransclem35  40981  sge0iunmptlemfi  41125  iundjiun  41172  meaiininclem  41198  hoidmvle  41312  ovnhoilem2  41314  smflimlem1  41477  smfrec  41494  smfliminflem  41534
  Copyright terms: Public domain W3C validator