MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nic-axALT Structured version   Visualization version   GIF version

Theorem nic-axALT 1597
Description: A direct proof of nic-ax 1596. (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 473 . . . . . 6 ((𝜒𝜓) → 𝜒)
21imim2i 16 . . . . 5 ((𝜑 → (𝜒𝜓)) → (𝜑𝜒))
3 con3 149 . . . . . 6 ((𝜑𝜒) → (¬ 𝜒 → ¬ 𝜑))
43imim2d 57 . . . . 5 ((𝜑𝜒) → ((𝜃 → ¬ 𝜒) → (𝜃 → ¬ 𝜑)))
52, 4syl 17 . . . 4 ((𝜑 → (𝜒𝜓)) → ((𝜃 → ¬ 𝜒) → (𝜃 → ¬ 𝜑)))
6 anidm 675 . . . . 5 ((𝜏𝜏) ↔ 𝜏)
76biimpri 218 . . . 4 (𝜏 → (𝜏𝜏))
85, 7jctil 559 . . 3 ((𝜑 → (𝜒𝜓)) → ((𝜏 → (𝜏𝜏)) ∧ ((𝜃 → ¬ 𝜒) → (𝜃 → ¬ 𝜑))))
9 df-nan 1446 . . . . . . . . 9 ((𝜒𝜓) ↔ ¬ (𝜒𝜓))
109anbi2i 729 . . . . . . . 8 ((𝜑 ∧ (𝜒𝜓)) ↔ (𝜑 ∧ ¬ (𝜒𝜓)))
1110notbii 310 . . . . . . 7 (¬ (𝜑 ∧ (𝜒𝜓)) ↔ ¬ (𝜑 ∧ ¬ (𝜒𝜓)))
12 df-nan 1446 . . . . . . 7 ((𝜑 ⊼ (𝜒𝜓)) ↔ ¬ (𝜑 ∧ (𝜒𝜓)))
13 iman 440 . . . . . . 7 ((𝜑 → (𝜒𝜓)) ↔ ¬ (𝜑 ∧ ¬ (𝜒𝜓)))
1411, 12, 133bitr4i 292 . . . . . 6 ((𝜑 ⊼ (𝜒𝜓)) ↔ (𝜑 → (𝜒𝜓)))
15 df-nan 1446 . . . . . . 7 (((𝜏 ⊼ (𝜏𝜏)) ⊼ ((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃)))) ↔ ¬ ((𝜏 ⊼ (𝜏𝜏)) ∧ ((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃)))))
16 df-nan 1446 . . . . . . . . . . 11 ((𝜏𝜏) ↔ ¬ (𝜏𝜏))
1716anbi2i 729 . . . . . . . . . 10 ((𝜏 ∧ (𝜏𝜏)) ↔ (𝜏 ∧ ¬ (𝜏𝜏)))
1817notbii 310 . . . . . . . . 9 (¬ (𝜏 ∧ (𝜏𝜏)) ↔ ¬ (𝜏 ∧ ¬ (𝜏𝜏)))
19 df-nan 1446 . . . . . . . . 9 ((𝜏 ⊼ (𝜏𝜏)) ↔ ¬ (𝜏 ∧ (𝜏𝜏)))
20 iman 440 . . . . . . . . 9 ((𝜏 → (𝜏𝜏)) ↔ ¬ (𝜏 ∧ ¬ (𝜏𝜏)))
2118, 19, 203bitr4i 292 . . . . . . . 8 ((𝜏 ⊼ (𝜏𝜏)) ↔ (𝜏 → (𝜏𝜏)))
22 df-nan 1446 . . . . . . . . . . . 12 ((𝜃𝜒) ↔ ¬ (𝜃𝜒))
23 imnan 438 . . . . . . . . . . . 12 ((𝜃 → ¬ 𝜒) ↔ ¬ (𝜃𝜒))
2422, 23bitr4i 267 . . . . . . . . . . 11 ((𝜃𝜒) ↔ (𝜃 → ¬ 𝜒))
25 df-nan 1446 . . . . . . . . . . . 12 (((𝜑𝜃) ⊼ (𝜑𝜃)) ↔ ¬ ((𝜑𝜃) ∧ (𝜑𝜃)))
26 anidm 675 . . . . . . . . . . . . 13 (((𝜑𝜃) ∧ (𝜑𝜃)) ↔ (𝜑𝜃))
27 df-nan 1446 . . . . . . . . . . . . 13 ((𝜑𝜃) ↔ ¬ (𝜑𝜃))
28 imnan 438 . . . . . . . . . . . . . 14 ((𝜑 → ¬ 𝜃) ↔ ¬ (𝜑𝜃))
29 con2b 349 . . . . . . . . . . . . . 14 ((𝜑 → ¬ 𝜃) ↔ (𝜃 → ¬ 𝜑))
3028, 29bitr3i 266 . . . . . . . . . . . . 13 (¬ (𝜑𝜃) ↔ (𝜃 → ¬ 𝜑))
3126, 27, 303bitri 286 . . . . . . . . . . . 12 (((𝜑𝜃) ∧ (𝜑𝜃)) ↔ (𝜃 → ¬ 𝜑))
3225, 31xchbinx 324 . . . . . . . . . . 11 (((𝜑𝜃) ⊼ (𝜑𝜃)) ↔ ¬ (𝜃 → ¬ 𝜑))
3324, 32anbi12i 732 . . . . . . . . . 10 (((𝜃𝜒) ∧ ((𝜑𝜃) ⊼ (𝜑𝜃))) ↔ ((𝜃 → ¬ 𝜒) ∧ ¬ (𝜃 → ¬ 𝜑)))
3433notbii 310 . . . . . . . . 9 (¬ ((𝜃𝜒) ∧ ((𝜑𝜃) ⊼ (𝜑𝜃))) ↔ ¬ ((𝜃 → ¬ 𝜒) ∧ ¬ (𝜃 → ¬ 𝜑)))
35 df-nan 1446 . . . . . . . . 9 (((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃))) ↔ ¬ ((𝜃𝜒) ∧ ((𝜑𝜃) ⊼ (𝜑𝜃))))
36 iman 440 . . . . . . . . 9 (((𝜃 → ¬ 𝜒) → (𝜃 → ¬ 𝜑)) ↔ ¬ ((𝜃 → ¬ 𝜒) ∧ ¬ (𝜃 → ¬ 𝜑)))
3734, 35, 363bitr4i 292 . . . . . . . 8 (((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃))) ↔ ((𝜃 → ¬ 𝜒) → (𝜃 → ¬ 𝜑)))
3821, 37anbi12i 732 . . . . . . 7 (((𝜏 ⊼ (𝜏𝜏)) ∧ ((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃)))) ↔ ((𝜏 → (𝜏𝜏)) ∧ ((𝜃 → ¬ 𝜒) → (𝜃 → ¬ 𝜑))))
3915, 38xchbinx 324 . . . . . 6 (((𝜏 ⊼ (𝜏𝜏)) ⊼ ((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃)))) ↔ ¬ ((𝜏 → (𝜏𝜏)) ∧ ((𝜃 → ¬ 𝜒) → (𝜃 → ¬ 𝜑))))
4014, 39anbi12i 732 . . . . 5 (((𝜑 ⊼ (𝜒𝜓)) ∧ ((𝜏 ⊼ (𝜏𝜏)) ⊼ ((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃))))) ↔ ((𝜑 → (𝜒𝜓)) ∧ ¬ ((𝜏 → (𝜏𝜏)) ∧ ((𝜃 → ¬ 𝜒) → (𝜃 → ¬ 𝜑)))))
4140notbii 310 . . . 4 (¬ ((𝜑 ⊼ (𝜒𝜓)) ∧ ((𝜏 ⊼ (𝜏𝜏)) ⊼ ((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃))))) ↔ ¬ ((𝜑 → (𝜒𝜓)) ∧ ¬ ((𝜏 → (𝜏𝜏)) ∧ ((𝜃 → ¬ 𝜒) → (𝜃 → ¬ 𝜑)))))
42 iman 440 . . . 4 (((𝜑 → (𝜒𝜓)) → ((𝜏 → (𝜏𝜏)) ∧ ((𝜃 → ¬ 𝜒) → (𝜃 → ¬ 𝜑)))) ↔ ¬ ((𝜑 → (𝜒𝜓)) ∧ ¬ ((𝜏 → (𝜏𝜏)) ∧ ((𝜃 → ¬ 𝜒) → (𝜃 → ¬ 𝜑)))))
4341, 42bitr4i 267 . . 3 (¬ ((𝜑 ⊼ (𝜒𝜓)) ∧ ((𝜏 ⊼ (𝜏𝜏)) ⊼ ((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃))))) ↔ ((𝜑 → (𝜒𝜓)) → ((𝜏 → (𝜏𝜏)) ∧ ((𝜃 → ¬ 𝜒) → (𝜃 → ¬ 𝜑)))))
448, 43mpbir 221 . 2 ¬ ((𝜑 ⊼ (𝜒𝜓)) ∧ ((𝜏 ⊼ (𝜏𝜏)) ⊼ ((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃)))))
45 df-nan 1446 . 2 (((𝜑 ⊼ (𝜒𝜓)) ⊼ ((𝜏 ⊼ (𝜏𝜏)) ⊼ ((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃))))) ↔ ¬ ((𝜑 ⊼ (𝜒𝜓)) ∧ ((𝜏 ⊼ (𝜏𝜏)) ⊼ ((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃))))))
4644, 45mpbir 221 1 ((𝜑 ⊼ (𝜒𝜓)) ⊼ ((𝜏 ⊼ (𝜏𝜏)) ⊼ ((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384  wnan 1445
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 197  df-an 386  df-nan 1446
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator