Metamath Proof Explorer


Theorem axinfprim

Description: ax-inf without distinct variable conditions or defined symbols. (New usage is discouraged.) (Contributed by Scott Fenton, 13-Oct-2010)

Ref Expression
Assertion axinfprim ¬ x ¬ y z ¬ y x ¬ y y x ¬ z y z ¬ z x

Proof

Step Hyp Ref Expression
1 axinfnd x y z y x y y x z y z z x
2 df-an y z z x ¬ y z ¬ z x
3 2 exbii z y z z x z ¬ y z ¬ z x
4 exnal z ¬ y z ¬ z x ¬ z y z ¬ z x
5 3 4 bitri z y z z x ¬ z y z ¬ z x
6 5 imbi2i y x z y z z x y x ¬ z y z ¬ z x
7 6 albii y y x z y z z x y y x ¬ z y z ¬ z x
8 7 anbi2i y x y y x z y z z x y x y y x ¬ z y z ¬ z x
9 df-an y x y y x ¬ z y z ¬ z x ¬ y x ¬ y y x ¬ z y z ¬ z x
10 8 9 bitri y x y y x z y z z x ¬ y x ¬ y y x ¬ z y z ¬ z x
11 10 imbi2i y z y x y y x z y z z x y z ¬ y x ¬ y y x ¬ z y z ¬ z x
12 11 exbii x y z y x y y x z y z z x x y z ¬ y x ¬ y y x ¬ z y z ¬ z x
13 df-ex x y z ¬ y x ¬ y y x ¬ z y z ¬ z x ¬ x ¬ y z ¬ y x ¬ y y x ¬ z y z ¬ z x
14 12 13 bitri x y z y x y y x z y z z x ¬ x ¬ y z ¬ y x ¬ y y x ¬ z y z ¬ z x
15 1 14 mpbi ¬ x ¬ y z ¬ y x ¬ y y x ¬ z y z ¬ z x