![]() |
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 878 reu6 3684 axprlem3 5380 ordelord 6339 f1dmex 7888 soseq 8090 omeulem2 8529 2pwuninel 9075 isumrpcl 15727 kqfvima 23079 caubl 24670 nbupgr 28290 nbumgrvtx 28292 umgr2adedgspth 28891 btwnconn1lem12 34674 omabs2 41643 sbcim2g 42802 ee21an 42996 |
Copyright terms: Public domain | W3C validator |