Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  jath Structured version   Visualization version   GIF version

Theorem jath 31947
Description: Closed form of ja 174. Proved using the completeness script. (Proof modification is discouraged.) (Contributed by Scott Fenton, 13-Dec-2021.)
Assertion
Ref Expression
jath ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))

Proof of Theorem jath
StepHypRef Expression
1 mth8 159 . . . 4 𝜑 → (¬ 𝜒 → ¬ (¬ 𝜑𝜒)))
2 pm2.21 121 . . . . . 6 (¬ (¬ 𝜑𝜒) → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))))
3 imim2 58 . . . . . 6 ((¬ (¬ 𝜑𝜒) → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))) → ((¬ 𝜒 → ¬ (¬ 𝜑𝜒)) → (¬ 𝜒 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))))))
42, 3ax-mp 5 . . . . 5 ((¬ 𝜒 → ¬ (¬ 𝜑𝜒)) → (¬ 𝜒 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))))
5 imim2 58 . . . . 5 (((¬ 𝜒 → ¬ (¬ 𝜑𝜒)) → (¬ 𝜒 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))))) → ((¬ 𝜑 → (¬ 𝜒 → ¬ (¬ 𝜑𝜒))) → (¬ 𝜑 → (¬ 𝜒 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))))))
64, 5ax-mp 5 . . . 4 ((¬ 𝜑 → (¬ 𝜒 → ¬ (¬ 𝜑𝜒))) → (¬ 𝜑 → (¬ 𝜒 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))))))
71, 6ax-mp 5 . . 3 𝜑 → (¬ 𝜒 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))))
8 ax-1 6 . . . . . . 7 (𝜒 → ((𝜑𝜓) → 𝜒))
9 ax-1 6 . . . . . . . 8 (((𝜑𝜓) → 𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))
10 imim2 58 . . . . . . . 8 ((((𝜑𝜓) → 𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))) → ((𝜒 → ((𝜑𝜓) → 𝜒)) → (𝜒 → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))))
119, 10ax-mp 5 . . . . . . 7 ((𝜒 → ((𝜑𝜓) → 𝜒)) → (𝜒 → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))))
128, 11ax-mp 5 . . . . . 6 (𝜒 → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))
13 ax-1 6 . . . . . . 7 (((𝜓𝜒) → ((𝜑𝜓) → 𝜒)) → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))))
14 imim2 58 . . . . . . 7 ((((𝜓𝜒) → ((𝜑𝜓) → 𝜒)) → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))) → ((𝜒 → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))) → (𝜒 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))))))
1513, 14ax-mp 5 . . . . . 6 ((𝜒 → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))) → (𝜒 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))))
1612, 15ax-mp 5 . . . . 5 (𝜒 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))))
17 pm2.61 183 . . . . 5 ((𝜒 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))) → ((¬ 𝜒 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))) → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))))
1816, 17ax-mp 5 . . . 4 ((¬ 𝜒 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))) → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))))
19 imim2 58 . . . 4 (((¬ 𝜒 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))) → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))) → ((¬ 𝜑 → (¬ 𝜒 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))))) → (¬ 𝜑 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))))))
2018, 19ax-mp 5 . . 3 ((¬ 𝜑 → (¬ 𝜒 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))))) → (¬ 𝜑 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))))
217, 20ax-mp 5 . 2 𝜑 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))))
22 mth8 159 . . . . . . 7 (𝜑 → (¬ 𝜓 → ¬ (𝜑𝜓)))
23 pm2.21 121 . . . . . . . . 9 (¬ (𝜑𝜓) → ((𝜑𝜓) → 𝜒))
24 imim2 58 . . . . . . . . 9 ((¬ (𝜑𝜓) → ((𝜑𝜓) → 𝜒)) → ((¬ 𝜓 → ¬ (𝜑𝜓)) → (¬ 𝜓 → ((𝜑𝜓) → 𝜒))))
2523, 24ax-mp 5 . . . . . . . 8 ((¬ 𝜓 → ¬ (𝜑𝜓)) → (¬ 𝜓 → ((𝜑𝜓) → 𝜒)))
26 imim2 58 . . . . . . . 8 (((¬ 𝜓 → ¬ (𝜑𝜓)) → (¬ 𝜓 → ((𝜑𝜓) → 𝜒))) → ((𝜑 → (¬ 𝜓 → ¬ (𝜑𝜓))) → (𝜑 → (¬ 𝜓 → ((𝜑𝜓) → 𝜒)))))
2725, 26ax-mp 5 . . . . . . 7 ((𝜑 → (¬ 𝜓 → ¬ (𝜑𝜓))) → (𝜑 → (¬ 𝜓 → ((𝜑𝜓) → 𝜒))))
2822, 27ax-mp 5 . . . . . 6 (𝜑 → (¬ 𝜓 → ((𝜑𝜓) → 𝜒)))
29 imim2 58 . . . . . . . 8 ((((𝜑𝜓) → 𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))) → ((¬ 𝜓 → ((𝜑𝜓) → 𝜒)) → (¬ 𝜓 → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))))
309, 29ax-mp 5 . . . . . . 7 ((¬ 𝜓 → ((𝜑𝜓) → 𝜒)) → (¬ 𝜓 → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))))
31 imim2 58 . . . . . . 7 (((¬ 𝜓 → ((𝜑𝜓) → 𝜒)) → (¬ 𝜓 → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))) → ((𝜑 → (¬ 𝜓 → ((𝜑𝜓) → 𝜒))) → (𝜑 → (¬ 𝜓 → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))))))
3230, 31ax-mp 5 . . . . . 6 ((𝜑 → (¬ 𝜓 → ((𝜑𝜓) → 𝜒))) → (𝜑 → (¬ 𝜓 → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))))
3328, 32ax-mp 5 . . . . 5 (𝜑 → (¬ 𝜓 → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))))
34 imim2 58 . . . . . . 7 ((((𝜓𝜒) → ((𝜑𝜓) → 𝜒)) → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))) → ((¬ 𝜓 → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))) → (¬ 𝜓 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))))))
3513, 34ax-mp 5 . . . . . 6 ((¬ 𝜓 → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))) → (¬ 𝜓 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))))
36 imim2 58 . . . . . 6 (((¬ 𝜓 → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))) → (¬ 𝜓 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))))) → ((𝜑 → (¬ 𝜓 → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))) → (𝜑 → (¬ 𝜓 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))))))
3735, 36ax-mp 5 . . . . 5 ((𝜑 → (¬ 𝜓 → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))) → (𝜑 → (¬ 𝜓 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))))))
3833, 37ax-mp 5 . . . 4 (𝜑 → (¬ 𝜓 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))))
39 mth8 159 . . . . . . . . 9 (𝜓 → (¬ 𝜒 → ¬ (𝜓𝜒)))
40 pm2.21 121 . . . . . . . . . . 11 (¬ (𝜓𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))
41 imim2 58 . . . . . . . . . . 11 ((¬ (𝜓𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))) → ((¬ 𝜒 → ¬ (𝜓𝜒)) → (¬ 𝜒 → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))))
4240, 41ax-mp 5 . . . . . . . . . 10 ((¬ 𝜒 → ¬ (𝜓𝜒)) → (¬ 𝜒 → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))))
43 imim2 58 . . . . . . . . . 10 (((¬ 𝜒 → ¬ (𝜓𝜒)) → (¬ 𝜒 → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))) → ((𝜓 → (¬ 𝜒 → ¬ (𝜓𝜒))) → (𝜓 → (¬ 𝜒 → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))))))
4442, 43ax-mp 5 . . . . . . . . 9 ((𝜓 → (¬ 𝜒 → ¬ (𝜓𝜒))) → (𝜓 → (¬ 𝜒 → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))))
4539, 44ax-mp 5 . . . . . . . 8 (𝜓 → (¬ 𝜒 → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))))
46 imim2 58 . . . . . . . . . 10 ((((𝜓𝜒) → ((𝜑𝜓) → 𝜒)) → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))) → ((¬ 𝜒 → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))) → (¬ 𝜒 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))))))
4713, 46ax-mp 5 . . . . . . . . 9 ((¬ 𝜒 → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))) → (¬ 𝜒 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))))
48 imim2 58 . . . . . . . . 9 (((¬ 𝜒 → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))) → (¬ 𝜒 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))))) → ((𝜓 → (¬ 𝜒 → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))) → (𝜓 → (¬ 𝜒 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))))))
4947, 48ax-mp 5 . . . . . . . 8 ((𝜓 → (¬ 𝜒 → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))) → (𝜓 → (¬ 𝜒 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))))))
5045, 49ax-mp 5 . . . . . . 7 (𝜓 → (¬ 𝜒 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))))
51 imim2 58 . . . . . . . 8 (((¬ 𝜒 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))) → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))) → ((𝜓 → (¬ 𝜒 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))))) → (𝜓 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))))))
5218, 51ax-mp 5 . . . . . . 7 ((𝜓 → (¬ 𝜒 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))))) → (𝜓 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))))
5350, 52ax-mp 5 . . . . . 6 (𝜓 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))))
54 pm2.61 183 . . . . . 6 ((𝜓 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))) → ((¬ 𝜓 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))) → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))))
5553, 54ax-mp 5 . . . . 5 ((¬ 𝜓 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))) → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))))
56 imim2 58 . . . . 5 (((¬ 𝜓 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))) → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))) → ((𝜑 → (¬ 𝜓 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))))) → (𝜑 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))))))
5755, 56ax-mp 5 . . . 4 ((𝜑 → (¬ 𝜓 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))))) → (𝜑 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))))
5838, 57ax-mp 5 . . 3 (𝜑 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))))
59 pm2.61 183 . . 3 ((𝜑 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))) → ((¬ 𝜑 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))) → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))))
6058, 59ax-mp 5 . 2 ((¬ 𝜑 → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))) → ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒))))
6121, 60ax-mp 5 1 ((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator