Metamath Proof Explorer

Theorem nic-axALT

Description: A direct proof of nic-ax . (Contributed by NM, 11-Dec-2008) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion nic-axALT 
|- ( ( ph -/\ ( ch -/\ ps ) ) -/\ ( ( ta -/\ ( ta -/\ ta ) ) -/\ ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( ch /\ ps ) -> ch )
2 1 imim2i 
 |-  ( ( ph -> ( ch /\ ps ) ) -> ( ph -> ch ) )
3 con3 
 |-  ( ( ph -> ch ) -> ( -. ch -> -. ph ) )
4 3 imim2d 
 |-  ( ( ph -> ch ) -> ( ( th -> -. ch ) -> ( th -> -. ph ) ) )
5 2 4 syl 
 |-  ( ( ph -> ( ch /\ ps ) ) -> ( ( th -> -. ch ) -> ( th -> -. ph ) ) )
6 anidm 
 |-  ( ( ta /\ ta ) <-> ta )
7 6 biimpri 
 |-  ( ta -> ( ta /\ ta ) )
8 5 7 jctil 
 |-  ( ( ph -> ( ch /\ ps ) ) -> ( ( ta -> ( ta /\ ta ) ) /\ ( ( th -> -. ch ) -> ( th -> -. ph ) ) ) )
9 df-nan 
 |-  ( ( ch -/\ ps ) <-> -. ( ch /\ ps ) )
10 9 anbi2i 
 |-  ( ( ph /\ ( ch -/\ ps ) ) <-> ( ph /\ -. ( ch /\ ps ) ) )
11 10 notbii 
 |-  ( -. ( ph /\ ( ch -/\ ps ) ) <-> -. ( ph /\ -. ( ch /\ ps ) ) )
12 df-nan 
 |-  ( ( ph -/\ ( ch -/\ ps ) ) <-> -. ( ph /\ ( ch -/\ ps ) ) )
13 iman 
 |-  ( ( ph -> ( ch /\ ps ) ) <-> -. ( ph /\ -. ( ch /\ ps ) ) )
14 11 12 13 3bitr4i 
 |-  ( ( ph -/\ ( ch -/\ ps ) ) <-> ( ph -> ( ch /\ ps ) ) )
15 df-nan 
 |-  ( ( ( ta -/\ ( ta -/\ ta ) ) -/\ ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) ) <-> -. ( ( ta -/\ ( ta -/\ ta ) ) /\ ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) ) )
16 df-nan 
 |-  ( ( ta -/\ ta ) <-> -. ( ta /\ ta ) )
17 16 anbi2i 
 |-  ( ( ta /\ ( ta -/\ ta ) ) <-> ( ta /\ -. ( ta /\ ta ) ) )
18 17 notbii 
 |-  ( -. ( ta /\ ( ta -/\ ta ) ) <-> -. ( ta /\ -. ( ta /\ ta ) ) )
19 df-nan 
 |-  ( ( ta -/\ ( ta -/\ ta ) ) <-> -. ( ta /\ ( ta -/\ ta ) ) )
20 iman 
 |-  ( ( ta -> ( ta /\ ta ) ) <-> -. ( ta /\ -. ( ta /\ ta ) ) )
21 18 19 20 3bitr4i 
 |-  ( ( ta -/\ ( ta -/\ ta ) ) <-> ( ta -> ( ta /\ ta ) ) )
22 df-nan 
 |-  ( ( th -/\ ch ) <-> -. ( th /\ ch ) )
23 imnan 
 |-  ( ( th -> -. ch ) <-> -. ( th /\ ch ) )
24 22 23 bitr4i 
 |-  ( ( th -/\ ch ) <-> ( th -> -. ch ) )
25 df-nan 
 |-  ( ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) <-> -. ( ( ph -/\ th ) /\ ( ph -/\ th ) ) )
26 anidm 
 |-  ( ( ( ph -/\ th ) /\ ( ph -/\ th ) ) <-> ( ph -/\ th ) )
27 df-nan 
 |-  ( ( ph -/\ th ) <-> -. ( ph /\ th ) )
28 imnan 
 |-  ( ( ph -> -. th ) <-> -. ( ph /\ th ) )
29 con2b 
 |-  ( ( ph -> -. th ) <-> ( th -> -. ph ) )
30 28 29 bitr3i 
 |-  ( -. ( ph /\ th ) <-> ( th -> -. ph ) )
31 26 27 30 3bitri 
 |-  ( ( ( ph -/\ th ) /\ ( ph -/\ th ) ) <-> ( th -> -. ph ) )
32 25 31 xchbinx 
 |-  ( ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) <-> -. ( th -> -. ph ) )
33 24 32 anbi12i 
 |-  ( ( ( th -/\ ch ) /\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) <-> ( ( th -> -. ch ) /\ -. ( th -> -. ph ) ) )
34 33 notbii 
 |-  ( -. ( ( th -/\ ch ) /\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) <-> -. ( ( th -> -. ch ) /\ -. ( th -> -. ph ) ) )
35 df-nan 
 |-  ( ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) <-> -. ( ( th -/\ ch ) /\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) )
36 iman 
 |-  ( ( ( th -> -. ch ) -> ( th -> -. ph ) ) <-> -. ( ( th -> -. ch ) /\ -. ( th -> -. ph ) ) )
37 34 35 36 3bitr4i 
 |-  ( ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) <-> ( ( th -> -. ch ) -> ( th -> -. ph ) ) )
38 21 37 anbi12i 
 |-  ( ( ( ta -/\ ( ta -/\ ta ) ) /\ ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) ) <-> ( ( ta -> ( ta /\ ta ) ) /\ ( ( th -> -. ch ) -> ( th -> -. ph ) ) ) )
39 15 38 xchbinx 
 |-  ( ( ( ta -/\ ( ta -/\ ta ) ) -/\ ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) ) <-> -. ( ( ta -> ( ta /\ ta ) ) /\ ( ( th -> -. ch ) -> ( th -> -. ph ) ) ) )
40 14 39 anbi12i 
 |-  ( ( ( ph -/\ ( ch -/\ ps ) ) /\ ( ( ta -/\ ( ta -/\ ta ) ) -/\ ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) ) ) <-> ( ( ph -> ( ch /\ ps ) ) /\ -. ( ( ta -> ( ta /\ ta ) ) /\ ( ( th -> -. ch ) -> ( th -> -. ph ) ) ) ) )
41 40 notbii 
 |-  ( -. ( ( ph -/\ ( ch -/\ ps ) ) /\ ( ( ta -/\ ( ta -/\ ta ) ) -/\ ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) ) ) <-> -. ( ( ph -> ( ch /\ ps ) ) /\ -. ( ( ta -> ( ta /\ ta ) ) /\ ( ( th -> -. ch ) -> ( th -> -. ph ) ) ) ) )
42 iman 
 |-  ( ( ( ph -> ( ch /\ ps ) ) -> ( ( ta -> ( ta /\ ta ) ) /\ ( ( th -> -. ch ) -> ( th -> -. ph ) ) ) ) <-> -. ( ( ph -> ( ch /\ ps ) ) /\ -. ( ( ta -> ( ta /\ ta ) ) /\ ( ( th -> -. ch ) -> ( th -> -. ph ) ) ) ) )
43 41 42 bitr4i 
 |-  ( -. ( ( ph -/\ ( ch -/\ ps ) ) /\ ( ( ta -/\ ( ta -/\ ta ) ) -/\ ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) ) ) <-> ( ( ph -> ( ch /\ ps ) ) -> ( ( ta -> ( ta /\ ta ) ) /\ ( ( th -> -. ch ) -> ( th -> -. ph ) ) ) ) )
44 8 43 mpbir 
 |-  -. ( ( ph -/\ ( ch -/\ ps ) ) /\ ( ( ta -/\ ( ta -/\ ta ) ) -/\ ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) ) )
45 df-nan 
 |-  ( ( ( ph -/\ ( ch -/\ ps ) ) -/\ ( ( ta -/\ ( ta -/\ ta ) ) -/\ ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) ) ) <-> -. ( ( ph -/\ ( ch -/\ ps ) ) /\ ( ( ta -/\ ( ta -/\ ta ) ) -/\ ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) ) ) )
46 44 45 mpbir 
 |-  ( ( ph -/\ ( ch -/\ ps ) ) -/\ ( ( ta -/\ ( ta -/\ ta ) ) -/\ ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) ) )