Step |
Hyp |
Ref |
Expression |
1 |
|
e222.1 |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) |
2 |
|
e222.2 |
⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) |
3 |
|
e222.3 |
⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) |
4 |
|
e222.4 |
⊢ ( 𝜒 → ( 𝜃 → ( 𝜏 → 𝜂 ) ) ) |
5 |
3
|
dfvd2i |
⊢ ( 𝜑 → ( 𝜓 → 𝜏 ) ) |
6 |
5
|
imp |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜏 ) |
7 |
1
|
dfvd2i |
⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) ) |
8 |
7
|
imp |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜒 ) |
9 |
2
|
dfvd2i |
⊢ ( 𝜑 → ( 𝜓 → 𝜃 ) ) |
10 |
9
|
imp |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜃 ) |
11 |
8 10 4
|
syl2im |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝜑 ∧ 𝜓 ) → ( 𝜏 → 𝜂 ) ) ) |
12 |
11
|
pm2.43i |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝜏 → 𝜂 ) ) |
13 |
6 12
|
syl5com |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝜑 ∧ 𝜓 ) → 𝜂 ) ) |
14 |
13
|
pm2.43i |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜂 ) |
15 |
14
|
ex |
⊢ ( 𝜑 → ( 𝜓 → 𝜂 ) ) |
16 |
15
|
dfvd2ir |
⊢ ( 𝜑 , 𝜓 ▶ 𝜂 ) |