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

Theorem syldbl2 841
Description: Stacked hypotheseis implies goal. (Contributed by Stanislas Polu, 9-Mar-2020.)
Hypothesis
Ref Expression
syldbl2.1 ((𝜑𝜓) → (𝜓𝜃))
Assertion
Ref Expression
syldbl2 ((𝜑𝜓) → 𝜃)

Proof of Theorem syldbl2
StepHypRef Expression
1 syldbl2.1 . . 3 ((𝜑𝜓) → (𝜓𝜃))
21com12 32 . 2 (𝜓 → ((𝜑𝜓) → 𝜃))
32anabsi7 671 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:  elpredimg  6338  rexdif1en  9197  php  9245  fpwwe2lem4  10672  elfzoextl  13757  rprmdvdspow  33541  rprmdvdsprod  33542  constrmon  33749  aks4d1p3  42060  primrootsunit1  42079  primrootlekpowne0  42087  sticksstones1  42128  sticksstones11  42138  unitscyglem2  42178  uspgrimprop  47811
  Copyright terms: Public domain W3C validator