Metamath Proof Explorer


Theorem axacprim

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

Ref Expression
Assertion axacprim ¬ x ¬ y z x ¬ y z ¬ z w ¬ w ¬ y ¬ ¬ w y z z w y w ¬ w x y = w ¬ y = w ¬ w y z z w y w ¬ w x

Proof

Step Hyp Ref Expression
1 axacnd x y z x y z z w w y w y z z w y w w x y = w
2 df-an y z z w ¬ y z ¬ z w
3 2 albii x y z z w x ¬ y z ¬ z w
4 anass y z z w y w w x y z z w y w w x
5 annim z w ¬ y w ¬ w x ¬ z w y w ¬ w x
6 pm4.63 ¬ y w ¬ w x y w w x
7 6 anbi2i z w ¬ y w ¬ w x z w y w w x
8 5 7 bitr3i ¬ z w y w ¬ w x z w y w w x
9 8 anbi2i y z ¬ z w y w ¬ w x y z z w y w w x
10 annim y z ¬ z w y w ¬ w x ¬ y z z w y w ¬ w x
11 4 9 10 3bitr2i y z z w y w w x ¬ y z z w y w ¬ w x
12 11 exbii w y z z w y w w x w ¬ y z z w y w ¬ w x
13 exnal w ¬ y z z w y w ¬ w x ¬ w y z z w y w ¬ w x
14 12 13 bitri w y z z w y w w x ¬ w y z z w y w ¬ w x
15 14 bibi1i w y z z w y w w x y = w ¬ w y z z w y w ¬ w x y = w
16 dfbi1 ¬ w y z z w y w ¬ w x y = w ¬ ¬ w y z z w y w ¬ w x y = w ¬ y = w ¬ w y z z w y w ¬ w x
17 15 16 bitri w y z z w y w w x y = w ¬ ¬ w y z z w y w ¬ w x y = w ¬ y = w ¬ w y z z w y w ¬ w x
18 17 albii y w y z z w y w w x y = w y ¬ ¬ w y z z w y w ¬ w x y = w ¬ y = w ¬ w y z z w y w ¬ w x
19 18 exbii w y w y z z w y w w x y = w w y ¬ ¬ w y z z w y w ¬ w x y = w ¬ y = w ¬ w y z z w y w ¬ w x
20 df-ex w y ¬ ¬ w y z z w y w ¬ w x y = w ¬ y = w ¬ w y z z w y w ¬ w x ¬ w ¬ y ¬ ¬ w y z z w y w ¬ w x y = w ¬ y = w ¬ w y z z w y w ¬ w x
21 19 20 bitri w y w y z z w y w w x y = w ¬ w ¬ y ¬ ¬ w y z z w y w ¬ w x y = w ¬ y = w ¬ w y z z w y w ¬ w x
22 3 21 imbi12i x y z z w w y w y z z w y w w x y = w x ¬ y z ¬ z w ¬ w ¬ y ¬ ¬ w y z z w y w ¬ w x y = w ¬ y = w ¬ w y z z w y w ¬ w x
23 22 2albii y z x y z z w w y w y z z w y w w x y = w y z x ¬ y z ¬ z w ¬ w ¬ y ¬ ¬ w y z z w y w ¬ w x y = w ¬ y = w ¬ w y z z w y w ¬ w x
24 23 exbii x y z x y z z w w y w y z z w y w w x y = w x y z x ¬ y z ¬ z w ¬ w ¬ y ¬ ¬ w y z z w y w ¬ w x y = w ¬ y = w ¬ w y z z w y w ¬ w x
25 df-ex x y z x ¬ y z ¬ z w ¬ w ¬ y ¬ ¬ w y z z w y w ¬ w x y = w ¬ y = w ¬ w y z z w y w ¬ w x ¬ x ¬ y z x ¬ y z ¬ z w ¬ w ¬ y ¬ ¬ w y z z w y w ¬ w x y = w ¬ y = w ¬ w y z z w y w ¬ w x
26 24 25 bitri x y z x y z z w w y w y z z w y w w x y = w ¬ x ¬ y z x ¬ y z ¬ z w ¬ w ¬ y ¬ ¬ w y z z w y w ¬ w x y = w ¬ y = w ¬ w y z z w y w ¬ w x
27 1 26 mpbi ¬ x ¬ y z x ¬ y z ¬ z w ¬ w ¬ y ¬ ¬ w y z z w y w ¬ w x y = w ¬ y = w ¬ w y z z w y w ¬ w x