Metamath Proof Explorer


Theorem syl6ib

Description: A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 21-Jun-1993)

Ref Expression
Hypotheses syl6ib.1 φψχ
syl6ib.2 χθ
Assertion syl6ib φψθ

Proof

Step Hyp Ref Expression
1 syl6ib.1 φψχ
2 syl6ib.2 χθ
3 2 biimpi χθ
4 1 3 syl6 φψθ