Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > ee222 | Structured version Visualization version GIF version |
Description: e222 40976 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 409 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
3 | ee222.2 | . . . 4 ⊢ (𝜑 → (𝜓 → 𝜃)) | |
4 | 3 | imp 409 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
5 | ee222.3 | . . . 4 ⊢ (𝜑 → (𝜓 → 𝜏)) | |
6 | 5 | imp 409 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜏) |
7 | ee222.4 | . . 3 ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) | |
8 | 2, 4, 6, 7 | syl3c 66 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜂) |
9 | 8 | ex 415 | 1 ⊢ (𝜑 → (𝜓 → 𝜂)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 |
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 |
This theorem is referenced by: ee121 40845 ee122 40846 tratrb 40876 ee220 40978 ee202 40980 ee022 40982 ee002 40984 ee020 40986 ee200 40988 ee221 40990 ee212 40992 ee112 40995 ee211 40998 ee210 41000 ee201 41002 ee120 41004 ee021 41006 ee012 41008 ee102 41010 suctrALT2 41177 |
Copyright terms: Public domain | W3C validator |