Metamath Proof Explorer


Theorem axc5c711

Description: Proof of a single axiom that can replace ax-c5 , ax-c7 , and ax-11 in a subsystem that includes these axioms plus ax-c4 and ax-gen (and propositional calculus). See axc5c711toc5 , axc5c711toc7 , and axc5c711to11 for the rederivation of those axioms. This theorem extends the idea in Scott Fenton's axc5c7 . (Contributed by NM, 18-Nov-2006) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion axc5c711 xy¬xyφxφφ

Proof

Step Hyp Ref Expression
1 ax-c5 yφφ
2 ax10fromc7 ¬yφy¬yφ
3 ax-c7 ¬x¬xyφyφ
4 3 con1i ¬yφx¬xyφ
5 4 alimi y¬yφyx¬xyφ
6 ax-11 yx¬xyφxy¬xyφ
7 2 5 6 3syl ¬yφxy¬xyφ
8 1 7 nsyl4 ¬xy¬xyφφ
9 ax-c5 xφφ
10 8 9 ja xy¬xyφxφφ