Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > ee222 | Structured version Visualization version GIF version |
Description: e222 38861 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 445 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
3 | ee222.2 | . . . 4 ⊢ (𝜑 → (𝜓 → 𝜃)) | |
4 | 3 | imp 445 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
5 | ee222.3 | . . . 4 ⊢ (𝜑 → (𝜓 → 𝜏)) | |
6 | 5 | imp 445 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜏) |
7 | ee222.4 | . . 3 ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) | |
8 | 2, 4, 6, 7 | syl3c 66 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜂) |
9 | 8 | ex 450 | 1 ⊢ (𝜑 → (𝜓 → 𝜂)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 384 |
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 197 df-an 386 |
This theorem is referenced by: ee121 38711 ee122 38712 tratrb 38746 ee220 38863 ee202 38865 ee022 38867 ee002 38869 ee020 38871 ee200 38873 ee221 38875 ee212 38877 ee112 38880 ee211 38883 ee210 38885 ee201 38887 ee120 38889 ee021 38891 ee012 38893 ee102 38895 suctrALT2 39072 |
Copyright terms: Public domain | W3C validator |