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  6335  rexdif1en  9199  php  9248  fpwwe2lem4  10675  elfzoextl  13761  rprmdvdspow  33562  rprmdvdsprod  33563  constrmon  33786  aks4d1p3  42080  primrootsunit1  42099  primrootlekpowne0  42107  sticksstones1  42148  sticksstones11  42158  unitscyglem2  42198  uspgrimprop  47878
  Copyright terms: Public domain W3C validator