![]() |
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 3723 axprlem3 5424 ordelord 6387 f1dmex 7943 soseq 8145 omeulem2 8583 2pwuninel 9132 isumrpcl 15789 kqfvima 23234 caubl 24825 nbupgr 28601 nbumgrvtx 28603 umgr2adedgspth 29202 btwnconn1lem12 35070 omabs2 42082 sbcim2g 43299 ee21an 43493 |
Copyright terms: Public domain | W3C validator |