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 873 reu6 3714 axprlem3 5316 ordelord 6206 f1dmex 7647 omeulem2 8198 2pwuninel 8660 isumrpcl 15186 kqfvima 22266 caubl 23838 nbupgr 27053 nbumgrvtx 27055 umgr2adedgspth 27654 soseq 32993 btwnconn1lem12 33456 sbcim2g 40749 ee21an 40943 |
Copyright terms: Public domain | W3C validator |