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

Theorem adantlll 749
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 475 . 2 ((𝜏𝜑) → 𝜑)
2 adantl2.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylanl1 679 1 ((((𝜏𝜑) ∧ 𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  fun11iun  6996  oewordri  7536  sbthlem8  7939  xmulass  11946  caucvgb  14204  clsnsg  21665  metustto  22109  constr3cycl  25955  grpoidinvlem3  26510  nmoub3i  26818  riesz3i  28111  csmdsymi  28383  finxpreclem3  32202  fin2so  32362  matunitlindflem1  32371  mblfinlem2  32413  mblfinlem3  32414  ismblfin  32416  itg2addnclem  32427  ftc1anclem7  32457  ftc1anc  32459  fzmul  32503  fdc  32507  incsequz2  32511  isbnd3  32549  bndss  32551  ismtyres  32573  rngoisocnv  32746  xralrple2  38308  xralrple3  38328  dirkertrigeq  38791  fourierdlem12  38809  fourierdlem50  38846  fourierdlem103  38899  fourierdlem104  38900  etransclem35  38959  sge0iunmptlemfi  39103  iundjiun  39150  meaiininclem  39173  hoidmvle  39287  ovnhoilem2  39289  smflimlem1  39454  smfrec  39471
  Copyright terms: Public domain W3C validator