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 486 . 2 ((𝜏𝜑) → 𝜑)
2 adantl2.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylanl1 679 1 ((((𝜏𝜑) ∧ 𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  ad4ant23  752  ad4ant24  753  ad4ant234  1176  fiunlem  7875  sbthlem8  9035  caucvgb  15565  metustto  23912  grpoidinvlem3  29451  nmoub3i  29718  riesz3i  31007  csmdsymi  31279  finxpreclem3  35867  fin2so  36068  matunitlindflem1  36077  mblfinlem2  36119  mblfinlem3  36120  ismblfin  36122  itg2addnclem  36132  ftc1anclem7  36160  ftc1anc  36162  fzmul  36203  fdc  36207  incsequz2  36211  isbnd3  36246  bndss  36248  ismtyres  36270  rngoisocnv  36443  xralrple2  43595  xralrple3  43615  cvgcaule  43734  limsupmnflem  43968  climrescn  43996  xlimliminflimsup  44110  dirkertrigeq  44349  fourierdlem12  44367  fourierdlem50  44404  fourierdlem103  44457  fourierdlem104  44458  etransclem35  44517  sge0iunmptlemfi  44661  iundjiun  44708  meaiininclem  44734  hoidmvle  44848  ovnhoilem2  44850  smflimlem1  45019  smfrec  45037  smfliminflem  45078
  Copyright terms: Public domain W3C validator