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

Theorem adantlll 717
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 488 . 2 ((𝜏𝜑) → 𝜑)
2 adantl2.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylanl1 679 1 ((((𝜏𝜑) ∧ 𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  ad4ant23  752  ad4ant24  753  ad4ant234  1172  fiunlem  7629  sbthlem8  8622  caucvgb  15031  metustto  23163  grpoidinvlem3  28292  nmoub3i  28559  riesz3i  29848  csmdsymi  30120  finxpreclem3  34805  fin2so  35037  matunitlindflem1  35046  mblfinlem2  35088  mblfinlem3  35089  ismblfin  35091  itg2addnclem  35101  ftc1anclem7  35129  ftc1anc  35131  fzmul  35172  fdc  35176  incsequz2  35180  isbnd3  35215  bndss  35217  ismtyres  35239  rngoisocnv  35412  xralrple2  41973  xralrple3  41993  limsupmnflem  42349  climrescn  42377  xlimliminflimsup  42491  dirkertrigeq  42730  fourierdlem12  42748  fourierdlem50  42785  fourierdlem103  42838  fourierdlem104  42839  etransclem35  42898  sge0iunmptlemfi  43039  iundjiun  43086  meaiininclem  43112  hoidmvle  43226  ovnhoilem2  43228  smflimlem1  43391  smfrec  43408  smfliminflem  43448
  Copyright terms: Public domain W3C validator