| 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 44605 | . . . . . 6 ⊢ (𝜑 → (𝜓 → 𝜏)) |
| 3 | 2 | imp 406 | . . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝜏) |
| 4 | e222.1 | . . . . . . . . 9 ⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) | |
| 5 | 4 | dfvd2i 44605 | . . . . . . . 8 ⊢ (𝜑 → (𝜓 → 𝜒)) |
| 6 | 5 | imp 406 | . . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
| 7 | e222.2 | . . . . . . . . 9 ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) | |
| 8 | 7 | dfvd2i 44605 | . . . . . . . 8 ⊢ (𝜑 → (𝜓 → 𝜃)) |
| 9 | 8 | imp 406 | . . . . . . 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 412 | . 2 ⊢ (𝜑 → (𝜓 → 𝜂)) |
| 16 | 15 | dfvd2ir 44606 | 1 ⊢ ( 𝜑 , 𝜓 ▶ 𝜂 ) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ( wvd2 44597 |
| 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 207 df-an 396 df-vd2 44598 |
| This theorem is referenced by: e220 44657 e202 44659 e022 44661 e002 44663 e020 44665 e200 44667 e221 44669 e212 44671 e122 44673 e112 44674 e121 44676 e211 44677 e22 44691 suctrALT2VD 44856 en3lplem2VD 44864 19.21a3con13vVD 44872 tratrbVD 44881 |
| Copyright terms: Public domain | W3C validator |