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 877 reu6 3665 axprlem3 5291 ordelord 6181 f1dmex 7640 omeulem2 8192 2pwuninel 8656 isumrpcl 15190 kqfvima 22335 caubl 23912 nbupgr 27134 nbumgrvtx 27136 umgr2adedgspth 27734 soseq 33209 btwnconn1lem12 33672 sbcim2g 41244 ee21an 41438 |
Copyright terms: Public domain | W3C validator |