Metamath Proof Explorer


Theorem hirstL-ax3

Description: The third axiom of a system called "L" but proven to be a theorem since set.mm uses a different third axiom. This is named hirst after Holly P. Hirst and Jeffry L. Hirst. Axiom A3 of Mendelson p. 35. (Contributed by Jarvin Udandy, 7-Feb-2015) (Proof modification is discouraged.)

Ref Expression
Assertion hirstL-ax3 ¬ φ ¬ ψ ¬ φ ψ φ

Proof

Step Hyp Ref Expression
1 pm4.64 ¬ φ ψ φ ψ
2 pm4.66 ¬ φ ¬ ψ φ ¬ ψ
3 pm2.64 φ ψ φ ¬ ψ φ
4 3 com12 φ ¬ ψ φ ψ φ
5 2 4 sylbi ¬ φ ¬ ψ φ ψ φ
6 1 5 syl5bi ¬ φ ¬ ψ ¬ φ ψ φ