Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > ee222 | Structured version Visualization version GIF version |
Description: e222 40847 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 407 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
3 | ee222.2 | . . . 4 ⊢ (𝜑 → (𝜓 → 𝜃)) | |
4 | 3 | imp 407 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
5 | ee222.3 | . . . 4 ⊢ (𝜑 → (𝜓 → 𝜏)) | |
6 | 5 | imp 407 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜏) |
7 | ee222.4 | . . 3 ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) | |
8 | 2, 4, 6, 7 | syl3c 66 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜂) |
9 | 8 | ex 413 | 1 ⊢ (𝜑 → (𝜓 → 𝜂)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 208 df-an 397 |
This theorem is referenced by: ee121 40716 ee122 40717 tratrb 40747 ee220 40849 ee202 40851 ee022 40853 ee002 40855 ee020 40857 ee200 40859 ee221 40861 ee212 40863 ee112 40866 ee211 40869 ee210 40871 ee201 40873 ee120 40875 ee021 40877 ee012 40879 ee102 40881 suctrALT2 41048 |
Copyright terms: Public domain | W3C validator |