![]() |
Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > ee222 | Structured version Visualization version GIF version |
Description: e222 43010 without virtual deduction connectives. Special theorem needed for the Virtual Deduction translation tool. (Contributed by Alan Sare, 7-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
ee222.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
ee222.2 | ⊢ (𝜑 → (𝜓 → 𝜃)) |
ee222.3 | ⊢ (𝜑 → (𝜓 → 𝜏)) |
ee222.4 | ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) |
Ref | Expression |
---|---|
ee222 | ⊢ (𝜑 → (𝜓 → 𝜂)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ee222.1 | . . . 4 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | 1 | imp 408 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
3 | ee222.2 | . . . 4 ⊢ (𝜑 → (𝜓 → 𝜃)) | |
4 | 3 | imp 408 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
5 | ee222.3 | . . . 4 ⊢ (𝜑 → (𝜓 → 𝜏)) | |
6 | 5 | imp 408 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜏) |
7 | ee222.4 | . . 3 ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) | |
8 | 2, 4, 6, 7 | syl3c 66 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜂) |
9 | 8 | ex 414 | 1 ⊢ (𝜑 → (𝜓 → 𝜂)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 |
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 |
This theorem is referenced by: ee121 42879 ee122 42880 tratrb 42910 ee220 43012 ee202 43014 ee022 43016 ee002 43018 ee020 43020 ee200 43022 ee221 43024 ee212 43026 ee112 43029 ee211 43032 ee210 43034 ee201 43036 ee120 43038 ee021 43040 ee012 43042 ee102 43044 suctrALT2 43211 |
Copyright terms: Public domain | W3C validator |