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 40939 | . . . . . 6 ⊢ (𝜑 → (𝜓 → 𝜏)) |
3 | 2 | imp 409 | . . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝜏) |
4 | e222.1 | . . . . . . . . 9 ⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) | |
5 | 4 | dfvd2i 40939 | . . . . . . . 8 ⊢ (𝜑 → (𝜓 → 𝜒)) |
6 | 5 | imp 409 | . . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
7 | e222.2 | . . . . . . . . 9 ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) | |
8 | 7 | dfvd2i 40939 | . . . . . . . 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 40940 | 1 ⊢ ( 𝜑 , 𝜓 ▶ 𝜂 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 ( wvd2 40931 |
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 40932 |
This theorem is referenced by: e220 40991 e202 40993 e022 40995 e002 40997 e020 40999 e200 41001 e221 41003 e212 41005 e122 41007 e112 41008 e121 41010 e211 41011 e22 41025 suctrALT2VD 41190 en3lplem2VD 41198 19.21a3con13vVD 41206 tratrbVD 41215 |
Copyright terms: Public domain | W3C validator |