|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > syl6ci | Structured version Visualization version GIF version | ||
| Description: A syllogism inference combined with contraction. (Contributed by Alan Sare, 18-Mar-2012.) | 
| Ref | Expression | 
|---|---|
| syl6ci.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) | 
| syl6ci.2 | ⊢ (𝜑 → 𝜃) | 
| syl6ci.3 | ⊢ (𝜒 → (𝜃 → 𝜏)) | 
| Ref | Expression | 
|---|---|
| syl6ci | ⊢ (𝜑 → (𝜓 → 𝜏)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | syl6ci.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
| 2 | syl6ci.2 | . . 3 ⊢ (𝜑 → 𝜃) | |
| 3 | 2 | a1d 25 | . 2 ⊢ (𝜑 → (𝜓 → 𝜃)) | 
| 4 | syl6ci.3 | . 2 ⊢ (𝜒 → (𝜃 → 𝜏)) | |
| 5 | 1, 3, 4 | syl6c 70 | 1 ⊢ (𝜑 → (𝜓 → 𝜏)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 | 
| This theorem is referenced by: mtord 879 reu6 3731 axprlem3OLD 5427 ordelord 6405 f1dmex 7982 soseq 8185 omeulem2 8622 2pwuninel 9173 isumrpcl 15880 kqfvima 23739 caubl 25343 nbupgr 29362 nbumgrvtx 29364 umgr2adedgspth 29969 btwnconn1lem12 36100 omabs2 43350 sbcim2g 44563 ee21an 44757 | 
| Copyright terms: Public domain | W3C validator |