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 40926 | . . . . . 6 ⊢ (𝜑 → (𝜓 → 𝜏)) |
3 | 2 | imp 409 | . . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝜏) |
4 | e222.1 | . . . . . . . . 9 ⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) | |
5 | 4 | dfvd2i 40926 | . . . . . . . 8 ⊢ (𝜑 → (𝜓 → 𝜒)) |
6 | 5 | imp 409 | . . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
7 | e222.2 | . . . . . . . . 9 ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) | |
8 | 7 | dfvd2i 40926 | . . . . . . . 8 ⊢ (𝜑 → (𝜓 → 𝜃)) |
9 | 8 | imp 409 | . . . . . . 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 415 | . 2 ⊢ (𝜑 → (𝜓 → 𝜂)) |
16 | 15 | dfvd2ir 40927 | 1 ⊢ ( 𝜑 , 𝜓 ▶ 𝜂 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 ( wvd2 40918 |
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 209 df-an 399 df-vd2 40919 |
This theorem is referenced by: e220 40978 e202 40980 e022 40982 e002 40984 e020 40986 e200 40988 e221 40990 e212 40992 e122 40994 e112 40995 e121 40997 e211 40998 e22 41012 suctrALT2VD 41177 en3lplem2VD 41185 19.21a3con13vVD 41193 tratrbVD 41202 |
Copyright terms: Public domain | W3C validator |