Metamath Proof Explorer


Theorem nic-bi2

Description: Inference to extract the other side of an implication from a 'biconditional' definition. (Contributed by Jeff Hoffman, 18-Nov-2007) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis nic-bi2.1 φ ψ φ φ ψ ψ
Assertion nic-bi2 ψ φ φ

Proof

Step Hyp Ref Expression
1 nic-bi2.1 φ ψ φ φ ψ ψ
2 1 nic-isw2 φ ψ ψ ψ φ φ
3 nic-id ψ ψ ψ
4 2 3 nic-iimp1 ψ φ ψ
5 4 nic-idel ψ φ φ