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 φψθ