![]() |
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 3735 axprlem3OLD 5434 ordelord 6408 f1dmex 7980 soseq 8183 omeulem2 8620 2pwuninel 9171 isumrpcl 15876 kqfvima 23754 caubl 25356 nbupgr 29376 nbumgrvtx 29378 umgr2adedgspth 29978 btwnconn1lem12 36080 omabs2 43322 sbcim2g 44536 ee21an 44730 |
Copyright terms: Public domain | W3C validator |