Metamath Proof Explorer


Theorem syldbl2

Description: Stacked hypotheseis implies goal. (Contributed by Stanislas Polu, 9-Mar-2020)

Ref Expression
Hypothesis syldbl2.1 ( ( 𝜑𝜓 ) → ( 𝜓𝜃 ) )
Assertion syldbl2 ( ( 𝜑𝜓 ) → 𝜃 )

Proof

Step Hyp Ref Expression
1 syldbl2.1 ( ( 𝜑𝜓 ) → ( 𝜓𝜃 ) )
2 1 com12 ( 𝜓 → ( ( 𝜑𝜓 ) → 𝜃 ) )
3 2 anabsi7 ( ( 𝜑𝜓 ) → 𝜃 )