NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  nic-axALT GIF version

Theorem nic-axALT 1439
Description: A direct proof of nic-ax 1438. (Contributed by NM, 11-Dec-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
nic-axALT ((φ (χ ψ)) ((τ (τ τ)) ((θ χ) ((φ θ) (φ θ)))))

Proof of Theorem nic-axALT
StepHypRef Expression
1 simpl 443 . . . . . 6 ((χ ψ) → χ)
21imim2i 13 . . . . 5 ((φ → (χ ψ)) → (φχ))
3 con3 126 . . . . . 6 ((φχ) → (¬ χ → ¬ φ))
43imim2d 48 . . . . 5 ((φχ) → ((θ → ¬ χ) → (θ → ¬ φ)))
52, 4syl 15 . . . 4 ((φ → (χ ψ)) → ((θ → ¬ χ) → (θ → ¬ φ)))
6 anidm 625 . . . . 5 ((τ τ) ↔ τ)
76biimpri 197 . . . 4 (τ → (τ τ))
85, 7jctil 523 . . 3 ((φ → (χ ψ)) → ((τ → (τ τ)) ((θ → ¬ χ) → (θ → ¬ φ))))
9 df-nan 1288 . . . . . . . . 9 ((χ ψ) ↔ ¬ (χ ψ))
109anbi2i 675 . . . . . . . 8 ((φ (χ ψ)) ↔ (φ ¬ (χ ψ)))
1110notbii 287 . . . . . . 7 (¬ (φ (χ ψ)) ↔ ¬ (φ ¬ (χ ψ)))
12 df-nan 1288 . . . . . . 7 ((φ (χ ψ)) ↔ ¬ (φ (χ ψ)))
13 iman 413 . . . . . . 7 ((φ → (χ ψ)) ↔ ¬ (φ ¬ (χ ψ)))
1411, 12, 133bitr4i 268 . . . . . 6 ((φ (χ ψ)) ↔ (φ → (χ ψ)))
15 df-nan 1288 . . . . . . 7 (((τ (τ τ)) ((θ χ) ((φ θ) (φ θ)))) ↔ ¬ ((τ (τ τ)) ((θ χ) ((φ θ) (φ θ)))))
16 df-nan 1288 . . . . . . . . . . 11 ((τ τ) ↔ ¬ (τ τ))
1716anbi2i 675 . . . . . . . . . 10 ((τ (τ τ)) ↔ (τ ¬ (τ τ)))
1817notbii 287 . . . . . . . . 9 (¬ (τ (τ τ)) ↔ ¬ (τ ¬ (τ τ)))
19 df-nan 1288 . . . . . . . . 9 ((τ (τ τ)) ↔ ¬ (τ (τ τ)))
20 iman 413 . . . . . . . . 9 ((τ → (τ τ)) ↔ ¬ (τ ¬ (τ τ)))
2118, 19, 203bitr4i 268 . . . . . . . 8 ((τ (τ τ)) ↔ (τ → (τ τ)))
22 df-nan 1288 . . . . . . . . . . . 12 ((θ χ) ↔ ¬ (θ χ))
23 imnan 411 . . . . . . . . . . . 12 ((θ → ¬ χ) ↔ ¬ (θ χ))
2422, 23bitr4i 243 . . . . . . . . . . 11 ((θ χ) ↔ (θ → ¬ χ))
25 df-nan 1288 . . . . . . . . . . . 12 (((φ θ) (φ θ)) ↔ ¬ ((φ θ) (φ θ)))
26 anidm 625 . . . . . . . . . . . . 13 (((φ θ) (φ θ)) ↔ (φ θ))
27 df-nan 1288 . . . . . . . . . . . . 13 ((φ θ) ↔ ¬ (φ θ))
28 imnan 411 . . . . . . . . . . . . . 14 ((φ → ¬ θ) ↔ ¬ (φ θ))
29 con2b 324 . . . . . . . . . . . . . 14 ((φ → ¬ θ) ↔ (θ → ¬ φ))
3028, 29bitr3i 242 . . . . . . . . . . . . 13 (¬ (φ θ) ↔ (θ → ¬ φ))
3126, 27, 303bitri 262 . . . . . . . . . . . 12 (((φ θ) (φ θ)) ↔ (θ → ¬ φ))
3225, 31xchbinx 301 . . . . . . . . . . 11 (((φ θ) (φ θ)) ↔ ¬ (θ → ¬ φ))
3324, 32anbi12i 678 . . . . . . . . . 10 (((θ χ) ((φ θ) (φ θ))) ↔ ((θ → ¬ χ) ¬ (θ → ¬ φ)))
3433notbii 287 . . . . . . . . 9 (¬ ((θ χ) ((φ θ) (φ θ))) ↔ ¬ ((θ → ¬ χ) ¬ (θ → ¬ φ)))
35 df-nan 1288 . . . . . . . . 9 (((θ χ) ((φ θ) (φ θ))) ↔ ¬ ((θ χ) ((φ θ) (φ θ))))
36 iman 413 . . . . . . . . 9 (((θ → ¬ χ) → (θ → ¬ φ)) ↔ ¬ ((θ → ¬ χ) ¬ (θ → ¬ φ)))
3734, 35, 363bitr4i 268 . . . . . . . 8 (((θ χ) ((φ θ) (φ θ))) ↔ ((θ → ¬ χ) → (θ → ¬ φ)))
3821, 37anbi12i 678 . . . . . . 7 (((τ (τ τ)) ((θ χ) ((φ θ) (φ θ)))) ↔ ((τ → (τ τ)) ((θ → ¬ χ) → (θ → ¬ φ))))
3915, 38xchbinx 301 . . . . . 6 (((τ (τ τ)) ((θ χ) ((φ θ) (φ θ)))) ↔ ¬ ((τ → (τ τ)) ((θ → ¬ χ) → (θ → ¬ φ))))
4014, 39anbi12i 678 . . . . 5 (((φ (χ ψ)) ((τ (τ τ)) ((θ χ) ((φ θ) (φ θ))))) ↔ ((φ → (χ ψ)) ¬ ((τ → (τ τ)) ((θ → ¬ χ) → (θ → ¬ φ)))))
4140notbii 287 . . . 4 (¬ ((φ (χ ψ)) ((τ (τ τ)) ((θ χ) ((φ θ) (φ θ))))) ↔ ¬ ((φ → (χ ψ)) ¬ ((τ → (τ τ)) ((θ → ¬ χ) → (θ → ¬ φ)))))
42 iman 413 . . . 4 (((φ → (χ ψ)) → ((τ → (τ τ)) ((θ → ¬ χ) → (θ → ¬ φ)))) ↔ ¬ ((φ → (χ ψ)) ¬ ((τ → (τ τ)) ((θ → ¬ χ) → (θ → ¬ φ)))))
4341, 42bitr4i 243 . . 3 (¬ ((φ (χ ψ)) ((τ (τ τ)) ((θ χ) ((φ θ) (φ θ))))) ↔ ((φ → (χ ψ)) → ((τ → (τ τ)) ((θ → ¬ χ) → (θ → ¬ φ)))))
448, 43mpbir 200 . 2 ¬ ((φ (χ ψ)) ((τ (τ τ)) ((θ χ) ((φ θ) (φ θ)))))
45 df-nan 1288 . 2 (((φ (χ ψ)) ((τ (τ τ)) ((θ χ) ((φ θ) (φ θ))))) ↔ ¬ ((φ (χ ψ)) ((τ (τ τ)) ((θ χ) ((φ θ) (φ θ))))))
4644, 45mpbir 200 1 ((φ (χ ψ)) ((τ (τ τ)) ((θ χ) ((φ θ) (φ θ)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   wa 358   wnan 1287
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-nan 1288
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator