Proof of Theorem eel12131
Step | Hyp | Ref
| Expression |
1 | | eel12131.3 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜏) → 𝜂) |
2 | | eel12131.2 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
3 | | eel12131.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝜓) |
4 | | eel12131.4 |
. . . . . . . . . . . 12
⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁) |
5 | 4 | 3exp 1256 |
. . . . . . . . . . 11
⊢ (𝜓 → (𝜃 → (𝜂 → 𝜁))) |
6 | 3, 5 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝜃 → (𝜂 → 𝜁))) |
7 | 2, 6 | syl5com 31 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜒) → (𝜑 → (𝜂 → 𝜁))) |
8 | 7 | ex 449 |
. . . . . . . 8
⊢ (𝜑 → (𝜒 → (𝜑 → (𝜂 → 𝜁)))) |
9 | 8 | pm2.43b 53 |
. . . . . . 7
⊢ (𝜒 → (𝜑 → (𝜂 → 𝜁))) |
10 | 9 | com13 86 |
. . . . . 6
⊢ (𝜂 → (𝜑 → (𝜒 → 𝜁))) |
11 | 1, 10 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝜏) → (𝜑 → (𝜒 → 𝜁))) |
12 | 11 | ex 449 |
. . . 4
⊢ (𝜑 → (𝜏 → (𝜑 → (𝜒 → 𝜁)))) |
13 | 12 | pm2.43b 53 |
. . 3
⊢ (𝜏 → (𝜑 → (𝜒 → 𝜁))) |
14 | 13 | com3l 87 |
. 2
⊢ (𝜑 → (𝜒 → (𝜏 → 𝜁))) |
15 | 14 | 3imp 1249 |
1
⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁) |