Metamath Proof Explorer


Theorem albi

Description: Theorem 19.15 of Margaris p. 90. (Contributed by NM, 24-Jan-1993)

Ref Expression
Assertion albi xφψxφxψ

Proof

Step Hyp Ref Expression
1 biimp φψφψ
2 1 al2imi xφψxφxψ
3 biimpr φψψφ
4 3 al2imi xφψxψxφ
5 2 4 impbid xφψxφxψ