Proof of Theorem 3impexpVD
Step | Hyp | Ref
| Expression |
1 | | idn1 41752 |
. . . . . 6
⊢ ( ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ▶ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ) |
2 | | df-3an 1090 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) |
3 | | imbi1 351 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) → (((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ↔ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃))) |
4 | 3 | biimpcd 252 |
. . . . . 6
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) → (((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) → (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃))) |
5 | 1, 2, 4 | e10 41872 |
. . . . 5
⊢ ( ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ▶ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ) |
6 | | pm3.3 452 |
. . . . 5
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) → ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))) |
7 | 5, 6 | e1a 41805 |
. . . 4
⊢ ( ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ▶ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) ) |
8 | | pm3.3 452 |
. . . 4
⊢ (((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) → (𝜑 → (𝜓 → (𝜒 → 𝜃)))) |
9 | 7, 8 | e1a 41805 |
. . 3
⊢ ( ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ▶ (𝜑 → (𝜓 → (𝜒 → 𝜃))) ) |
10 | 9 | in1 41749 |
. 2
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) → (𝜑 → (𝜓 → (𝜒 → 𝜃)))) |
11 | | idn1 41752 |
. . . . . 6
⊢ ( (𝜑 → (𝜓 → (𝜒 → 𝜃))) ▶ (𝜑 → (𝜓 → (𝜒 → 𝜃))) ) |
12 | | pm3.31 453 |
. . . . . 6
⊢ ((𝜑 → (𝜓 → (𝜒 → 𝜃))) → ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))) |
13 | 11, 12 | e1a 41805 |
. . . . 5
⊢ ( (𝜑 → (𝜓 → (𝜒 → 𝜃))) ▶ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) ) |
14 | | pm3.31 453 |
. . . . 5
⊢ (((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) → (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)) |
15 | 13, 14 | e1a 41805 |
. . . 4
⊢ ( (𝜑 → (𝜓 → (𝜒 → 𝜃))) ▶ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ) |
16 | 3 | biimprd 251 |
. . . 4
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) → ((((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) → ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃))) |
17 | 2, 15, 16 | e01 41869 |
. . 3
⊢ ( (𝜑 → (𝜓 → (𝜒 → 𝜃))) ▶ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ) |
18 | 17 | in1 41749 |
. 2
⊢ ((𝜑 → (𝜓 → (𝜒 → 𝜃))) → ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)) |
19 | | impbi 211 |
. 2
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) → (𝜑 → (𝜓 → (𝜒 → 𝜃)))) → (((𝜑 → (𝜓 → (𝜒 → 𝜃))) → ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)) → (((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ↔ (𝜑 → (𝜓 → (𝜒 → 𝜃)))))) |
20 | 10, 18, 19 | e00 41946 |
1
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ↔ (𝜑 → (𝜓 → (𝜒 → 𝜃)))) |