Metamath Proof Explorer


Theorem bi33imp12

Description: 3imp with innermost implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017)

Ref Expression
Hypothesis bi33imp12.1 φψχθ
Assertion bi33imp12 φψχθ

Proof

Step Hyp Ref Expression
1 bi33imp12.1 φψχθ
2 biimp χθχθ
3 1 2 syl6 φψχθ
4 3 3imp φψχθ