![]() |
Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > e222 | Structured version Visualization version GIF version |
Description: A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
e222.1 | ⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) |
e222.2 | ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) |
e222.3 | ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) |
e222.4 | ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) |
Ref | Expression |
---|---|
e222 | ⊢ ( 𝜑 , 𝜓 ▶ 𝜂 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | e222.3 | . . . . . . 7 ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) | |
2 | 1 | dfvd2i 41291 | . . . . . 6 ⊢ (𝜑 → (𝜓 → 𝜏)) |
3 | 2 | imp 410 | . . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝜏) |
4 | e222.1 | . . . . . . . . 9 ⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) | |
5 | 4 | dfvd2i 41291 | . . . . . . . 8 ⊢ (𝜑 → (𝜓 → 𝜒)) |
6 | 5 | imp 410 | . . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
7 | e222.2 | . . . . . . . . 9 ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) | |
8 | 7 | dfvd2i 41291 | . . . . . . . 8 ⊢ (𝜑 → (𝜓 → 𝜃)) |
9 | 8 | imp 410 | . . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
10 | e222.4 | . . . . . . 7 ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) | |
11 | 6, 9, 10 | syl2im 40 | . . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → ((𝜑 ∧ 𝜓) → (𝜏 → 𝜂))) |
12 | 11 | pm2.43i 52 | . . . . 5 ⊢ ((𝜑 ∧ 𝜓) → (𝜏 → 𝜂)) |
13 | 3, 12 | syl5com 31 | . . . 4 ⊢ ((𝜑 ∧ 𝜓) → ((𝜑 ∧ 𝜓) → 𝜂)) |
14 | 13 | pm2.43i 52 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜂) |
15 | 14 | ex 416 | . 2 ⊢ (𝜑 → (𝜓 → 𝜂)) |
16 | 15 | dfvd2ir 41292 | 1 ⊢ ( 𝜑 , 𝜓 ▶ 𝜂 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ( wvd2 41283 |
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 210 df-an 400 df-vd2 41284 |
This theorem is referenced by: e220 41343 e202 41345 e022 41347 e002 41349 e020 41351 e200 41353 e221 41355 e212 41357 e122 41359 e112 41360 e121 41362 e211 41363 e22 41377 suctrALT2VD 41542 en3lplem2VD 41550 19.21a3con13vVD 41558 tratrbVD 41567 |
Copyright terms: Public domain | W3C validator |