Metamath Proof Explorer


Theorem ax3h

Description: Recover ax-3 from hirstL-ax3 . (Contributed by Jarvin Udandy, 3-Jul-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ax3h ¬ φ ¬ ψ ψ φ

Proof

Step Hyp Ref Expression
1 hirstL-ax3 ¬ φ ¬ ψ ¬ φ ψ φ
2 jarr ¬ φ ψ φ ψ φ
3 1 2 syl ¬ φ ¬ ψ ψ φ