Metamath Proof Explorer


Theorem sylancbr

Description: A syllogism inference combined with contraction. (Contributed by NM, 3-Sep-2004)

Ref Expression
Hypotheses sylancbr.1 ( 𝜓𝜑 )
sylancbr.2 ( 𝜒𝜑 )
sylancbr.3 ( ( 𝜓𝜒 ) → 𝜃 )
Assertion sylancbr ( 𝜑𝜃 )

Proof

Step Hyp Ref Expression
1 sylancbr.1 ( 𝜓𝜑 )
2 sylancbr.2 ( 𝜒𝜑 )
3 sylancbr.3 ( ( 𝜓𝜒 ) → 𝜃 )
4 1 2 3 syl2anbr ( ( 𝜑𝜑 ) → 𝜃 )
5 4 anidms ( 𝜑𝜃 )