Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > ee222 | Structured version Visualization version GIF version |
Description: e222 41870 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 410 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
3 | ee222.2 | . . . 4 ⊢ (𝜑 → (𝜓 → 𝜃)) | |
4 | 3 | imp 410 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
5 | ee222.3 | . . . 4 ⊢ (𝜑 → (𝜓 → 𝜏)) | |
6 | 5 | imp 410 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜏) |
7 | ee222.4 | . . 3 ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) | |
8 | 2, 4, 6, 7 | syl3c 66 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜂) |
9 | 8 | ex 416 | 1 ⊢ (𝜑 → (𝜓 → 𝜂)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 |
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 210 df-an 400 |
This theorem is referenced by: ee121 41739 ee122 41740 tratrb 41770 ee220 41872 ee202 41874 ee022 41876 ee002 41878 ee020 41880 ee200 41882 ee221 41884 ee212 41886 ee112 41889 ee211 41892 ee210 41894 ee201 41896 ee120 41898 ee021 41900 ee012 41902 ee102 41904 suctrALT2 42071 |
Copyright terms: Public domain | W3C validator |