Metamath Proof Explorer


Theorem imsym1

Description: A symmetry with -> .

See negsym1 for more information. (Contributed by Anthony Hart, 4-Sep-2011)

Ref Expression
Assertion imsym1 ψ ψ ψ φ

Proof

Step Hyp Ref Expression
1 pm2.21 ¬ ψ ψ φ
2 falim φ
3 2 imim2i ψ ψ φ
4 1 3 ja ψ ψ ψ φ