|   | Mathbox for Alan Sare | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > Mathboxes > ee222 | Structured version Visualization version GIF version | ||
| Description: e222 44656 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 406 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | 
| 3 | ee222.2 | . . . 4 ⊢ (𝜑 → (𝜓 → 𝜃)) | |
| 4 | 3 | imp 406 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜃) | 
| 5 | ee222.3 | . . . 4 ⊢ (𝜑 → (𝜓 → 𝜏)) | |
| 6 | 5 | imp 406 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜏) | 
| 7 | ee222.4 | . . 3 ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) | |
| 8 | 2, 4, 6, 7 | syl3c 66 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜂) | 
| 9 | 8 | ex 412 | 1 ⊢ (𝜑 → (𝜓 → 𝜂)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 | 
| 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 207 df-an 396 | 
| This theorem is referenced by: ee121 44525 ee122 44526 tratrb 44556 ee220 44658 ee202 44660 ee022 44662 ee002 44664 ee020 44666 ee200 44668 ee221 44670 ee212 44672 ee112 44675 ee211 44678 ee210 44680 ee201 44682 ee120 44684 ee021 44686 ee012 44688 ee102 44690 suctrALT2 44857 | 
| Copyright terms: Public domain | W3C validator |