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 ( ( 𝜓 → ( 𝜓 → ⊥ ) ) → ( 𝜓𝜑 ) )