![]() |
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 42772 | . . . . . 6 ⊢ (𝜑 → (𝜓 → 𝜏)) |
3 | 2 | imp 408 | . . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝜏) |
4 | e222.1 | . . . . . . . . 9 ⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) | |
5 | 4 | dfvd2i 42772 | . . . . . . . 8 ⊢ (𝜑 → (𝜓 → 𝜒)) |
6 | 5 | imp 408 | . . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
7 | e222.2 | . . . . . . . . 9 ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) | |
8 | 7 | dfvd2i 42772 | . . . . . . . 8 ⊢ (𝜑 → (𝜓 → 𝜃)) |
9 | 8 | imp 408 | . . . . . . 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 414 | . 2 ⊢ (𝜑 → (𝜓 → 𝜂)) |
16 | 15 | dfvd2ir 42773 | 1 ⊢ ( 𝜑 , 𝜓 ▶ 𝜂 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ( wvd2 42764 |
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 206 df-an 398 df-vd2 42765 |
This theorem is referenced by: e220 42824 e202 42826 e022 42828 e002 42830 e020 42832 e200 42834 e221 42836 e212 42838 e122 42840 e112 42841 e121 42843 e211 42844 e22 42858 suctrALT2VD 43023 en3lplem2VD 43031 19.21a3con13vVD 43039 tratrbVD 43048 |
Copyright terms: Public domain | W3C validator |