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 1666
Description: A direct proof of nic-ax 1665. (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 483 . . . . . 6 ((𝜒𝜓) → 𝜒)
21imim2i 16 . . . . 5 ((𝜑 → (𝜒𝜓)) → (𝜑𝜒))
3 con3 156 . . . . . 6 ((𝜑𝜒) → (¬ 𝜒 → ¬ 𝜑))
43imim2d 57 . . . . 5 ((𝜑𝜒) → ((𝜃 → ¬ 𝜒) → (𝜃 → ¬ 𝜑)))
52, 4syl 17 . . . 4 ((𝜑 → (𝜒𝜓)) → ((𝜃 → ¬ 𝜒) → (𝜃 → ¬ 𝜑)))
6 anidm 565 . . . . 5 ((𝜏𝜏) ↔ 𝜏)
76biimpri 229 . . . 4 (𝜏 → (𝜏𝜏))
85, 7jctil 520 . . 3 ((𝜑 → (𝜒𝜓)) → ((𝜏 → (𝜏𝜏)) ∧ ((𝜃 → ¬ 𝜒) → (𝜃 → ¬ 𝜑))))
9 df-nan 1476 . . . . . . . . 9 ((𝜒𝜓) ↔ ¬ (𝜒𝜓))
109anbi2i 622 . . . . . . . 8 ((𝜑 ∧ (𝜒𝜓)) ↔ (𝜑 ∧ ¬ (𝜒𝜓)))
1110notbii 321 . . . . . . 7 (¬ (𝜑 ∧ (𝜒𝜓)) ↔ ¬ (𝜑 ∧ ¬ (𝜒𝜓)))
12 df-nan 1476 . . . . . . 7 ((𝜑 ⊼ (𝜒𝜓)) ↔ ¬ (𝜑 ∧ (𝜒𝜓)))
13 iman 402 . . . . . . 7 ((𝜑 → (𝜒𝜓)) ↔ ¬ (𝜑 ∧ ¬ (𝜒𝜓)))
1411, 12, 133bitr4i 304 . . . . . 6 ((𝜑 ⊼ (𝜒𝜓)) ↔ (𝜑 → (𝜒𝜓)))
15 df-nan 1476 . . . . . . 7 (((𝜏 ⊼ (𝜏𝜏)) ⊼ ((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃)))) ↔ ¬ ((𝜏 ⊼ (𝜏𝜏)) ∧ ((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃)))))
16 df-nan 1476 . . . . . . . . . . 11 ((𝜏𝜏) ↔ ¬ (𝜏𝜏))
1716anbi2i 622 . . . . . . . . . 10 ((𝜏 ∧ (𝜏𝜏)) ↔ (𝜏 ∧ ¬ (𝜏𝜏)))
1817notbii 321 . . . . . . . . 9 (¬ (𝜏 ∧ (𝜏𝜏)) ↔ ¬ (𝜏 ∧ ¬ (𝜏𝜏)))
19 df-nan 1476 . . . . . . . . 9 ((𝜏 ⊼ (𝜏𝜏)) ↔ ¬ (𝜏 ∧ (𝜏𝜏)))
20 iman 402 . . . . . . . . 9 ((𝜏 → (𝜏𝜏)) ↔ ¬ (𝜏 ∧ ¬ (𝜏𝜏)))
2118, 19, 203bitr4i 304 . . . . . . . 8 ((𝜏 ⊼ (𝜏𝜏)) ↔ (𝜏 → (𝜏𝜏)))
22 df-nan 1476 . . . . . . . . . . . 12 ((𝜃𝜒) ↔ ¬ (𝜃𝜒))
23 imnan 400 . . . . . . . . . . . 12 ((𝜃 → ¬ 𝜒) ↔ ¬ (𝜃𝜒))
2422, 23bitr4i 279 . . . . . . . . . . 11 ((𝜃𝜒) ↔ (𝜃 → ¬ 𝜒))
25 df-nan 1476 . . . . . . . . . . . 12 (((𝜑𝜃) ⊼ (𝜑𝜃)) ↔ ¬ ((𝜑𝜃) ∧ (𝜑𝜃)))
26 anidm 565 . . . . . . . . . . . . 13 (((𝜑𝜃) ∧ (𝜑𝜃)) ↔ (𝜑𝜃))
27 df-nan 1476 . . . . . . . . . . . . 13 ((𝜑𝜃) ↔ ¬ (𝜑𝜃))
28 imnan 400 . . . . . . . . . . . . . 14 ((𝜑 → ¬ 𝜃) ↔ ¬ (𝜑𝜃))
29 con2b 361 . . . . . . . . . . . . . 14 ((𝜑 → ¬ 𝜃) ↔ (𝜃 → ¬ 𝜑))
3028, 29bitr3i 278 . . . . . . . . . . . . 13 (¬ (𝜑𝜃) ↔ (𝜃 → ¬ 𝜑))
3126, 27, 303bitri 298 . . . . . . . . . . . 12 (((𝜑𝜃) ∧ (𝜑𝜃)) ↔ (𝜃 → ¬ 𝜑))
3225, 31xchbinx 335 . . . . . . . . . . 11 (((𝜑𝜃) ⊼ (𝜑𝜃)) ↔ ¬ (𝜃 → ¬ 𝜑))
3324, 32anbi12i 626 . . . . . . . . . 10 (((𝜃𝜒) ∧ ((𝜑𝜃) ⊼ (𝜑𝜃))) ↔ ((𝜃 → ¬ 𝜒) ∧ ¬ (𝜃 → ¬ 𝜑)))
3433notbii 321 . . . . . . . . 9 (¬ ((𝜃𝜒) ∧ ((𝜑𝜃) ⊼ (𝜑𝜃))) ↔ ¬ ((𝜃 → ¬ 𝜒) ∧ ¬ (𝜃 → ¬ 𝜑)))
35 df-nan 1476 . . . . . . . . 9 (((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃))) ↔ ¬ ((𝜃𝜒) ∧ ((𝜑𝜃) ⊼ (𝜑𝜃))))
36 iman 402 . . . . . . . . 9 (((𝜃 → ¬ 𝜒) → (𝜃 → ¬ 𝜑)) ↔ ¬ ((𝜃 → ¬ 𝜒) ∧ ¬ (𝜃 → ¬ 𝜑)))
3734, 35, 363bitr4i 304 . . . . . . . 8 (((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃))) ↔ ((𝜃 → ¬ 𝜒) → (𝜃 → ¬ 𝜑)))
3821, 37anbi12i 626 . . . . . . 7 (((𝜏 ⊼ (𝜏𝜏)) ∧ ((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃)))) ↔ ((𝜏 → (𝜏𝜏)) ∧ ((𝜃 → ¬ 𝜒) → (𝜃 → ¬ 𝜑))))
3915, 38xchbinx 335 . . . . . 6 (((𝜏 ⊼ (𝜏𝜏)) ⊼ ((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃)))) ↔ ¬ ((𝜏 → (𝜏𝜏)) ∧ ((𝜃 → ¬ 𝜒) → (𝜃 → ¬ 𝜑))))
4014, 39anbi12i 626 . . . . 5 (((𝜑 ⊼ (𝜒𝜓)) ∧ ((𝜏 ⊼ (𝜏𝜏)) ⊼ ((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃))))) ↔ ((𝜑 → (𝜒𝜓)) ∧ ¬ ((𝜏 → (𝜏𝜏)) ∧ ((𝜃 → ¬ 𝜒) → (𝜃 → ¬ 𝜑)))))
4140notbii 321 . . . 4 (¬ ((𝜑 ⊼ (𝜒𝜓)) ∧ ((𝜏 ⊼ (𝜏𝜏)) ⊼ ((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃))))) ↔ ¬ ((𝜑 → (𝜒𝜓)) ∧ ¬ ((𝜏 → (𝜏𝜏)) ∧ ((𝜃 → ¬ 𝜒) → (𝜃 → ¬ 𝜑)))))
42 iman 402 . . . 4 (((𝜑 → (𝜒𝜓)) → ((𝜏 → (𝜏𝜏)) ∧ ((𝜃 → ¬ 𝜒) → (𝜃 → ¬ 𝜑)))) ↔ ¬ ((𝜑 → (𝜒𝜓)) ∧ ¬ ((𝜏 → (𝜏𝜏)) ∧ ((𝜃 → ¬ 𝜒) → (𝜃 → ¬ 𝜑)))))
4341, 42bitr4i 279 . . 3 (¬ ((𝜑 ⊼ (𝜒𝜓)) ∧ ((𝜏 ⊼ (𝜏𝜏)) ⊼ ((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃))))) ↔ ((𝜑 → (𝜒𝜓)) → ((𝜏 → (𝜏𝜏)) ∧ ((𝜃 → ¬ 𝜒) → (𝜃 → ¬ 𝜑)))))
448, 43mpbir 232 . 2 ¬ ((𝜑 ⊼ (𝜒𝜓)) ∧ ((𝜏 ⊼ (𝜏𝜏)) ⊼ ((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃)))))
45 df-nan 1476 . 2 (((𝜑 ⊼ (𝜒𝜓)) ⊼ ((𝜏 ⊼ (𝜏𝜏)) ⊼ ((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃))))) ↔ ¬ ((𝜑 ⊼ (𝜒𝜓)) ∧ ((𝜏 ⊼ (𝜏𝜏)) ⊼ ((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃))))))
4644, 45mpbir 232 1 ((𝜑 ⊼ (𝜒𝜓)) ⊼ ((𝜏 ⊼ (𝜏𝜏)) ⊼ ((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  wnan 1475
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 208  df-an 397  df-nan 1476
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator