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  1184  fun11iun  7292  oewordri  7843  sbthlem8  8244  xmulass  12330  caucvgb  14629  clsnsg  22134  metustto  22579  grpoidinvlem3  27690  nmoub3i  27958  riesz3i  29251  csmdsymi  29523  finxpreclem3  33559  fin2so  33727  matunitlindflem1  33736  mblfinlem2  33778  mblfinlem3  33779  ismblfin  33781  itg2addnclem  33792  ftc1anclem7  33822  ftc1anc  33824  fzmul  33868  fdc  33872  incsequz2  33876  isbnd3  33914  bndss  33916  ismtyres  33938  rngoisocnv  34111  xralrple2  40086  xralrple3  40106  limsupmnflem  40473  climrescn  40501  dirkertrigeq  40839  fourierdlem12  40857  fourierdlem50  40894  fourierdlem103  40947  fourierdlem104  40948  etransclem35  41007  sge0iunmptlemfi  41151  iundjiun  41198  meaiininclem  41224  hoidmvle  41338  ovnhoilem2  41340  smflimlem1  41503  smfrec  41520  smfliminflem  41560
  Copyright terms: Public domain W3C validator