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

Theorem adantlll 718
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 484 . 2 ((𝜏𝜑) → 𝜑)
2 adantl2.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylanl1 680 1 ((((𝜏𝜑) ∧ 𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  ad4ant23  753  ad4ant24  754  ad4ant234  1176  fiunlem  7966  sbthlem8  9130  caucvgb  15716  metustto  24566  grpoidinvlem3  30525  nmoub3i  30792  riesz3i  32081  csmdsymi  32353  finxpreclem3  37394  fin2so  37614  matunitlindflem1  37623  mblfinlem2  37665  mblfinlem3  37666  ismblfin  37668  itg2addnclem  37678  ftc1anclem7  37706  ftc1anc  37708  fzmul  37748  fdc  37752  incsequz2  37756  isbnd3  37791  bndss  37793  ismtyres  37815  rngoisocnv  37988  xralrple2  45365  xralrple3  45385  cvgcaule  45502  limsupmnflem  45735  climrescn  45763  xlimliminflimsup  45877  dirkertrigeq  46116  fourierdlem12  46134  fourierdlem50  46171  fourierdlem103  46224  fourierdlem104  46225  etransclem35  46284  sge0iunmptlemfi  46428  iundjiun  46475  meaiininclem  46501  hoidmvle  46615  ovnhoilem2  46617  smflimlem1  46786  smfrec  46804  smfliminflem  46845
  Copyright terms: Public domain W3C validator