Metamath Proof Explorer


Theorem biimp3ar

Description: Infer implication from a logical equivalence. Similar to biimpar . (Contributed by NM, 2-Jan-2009)

Ref Expression
Hypothesis biimp3a.1 φ ψ χ θ
Assertion biimp3ar φ ψ θ χ

Proof

Step Hyp Ref Expression
1 biimp3a.1 φ ψ χ θ
2 1 exbiri φ ψ θ χ
3 2 3imp φ ψ θ χ