![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > syl6c | Structured version Visualization version GIF version |
Description: Inference combining syl6 35 with contraction. (Contributed by Alan Sare, 2-May-2011.) |
Ref | Expression |
---|---|
syl6c.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
syl6c.2 | ⊢ (𝜑 → (𝜓 → 𝜃)) |
syl6c.3 | ⊢ (𝜒 → (𝜃 → 𝜏)) |
Ref | Expression |
---|---|
syl6c | ⊢ (𝜑 → (𝜓 → 𝜏)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl6c.2 | . 2 ⊢ (𝜑 → (𝜓 → 𝜃)) | |
2 | syl6c.1 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
3 | syl6c.3 | . . 3 ⊢ (𝜒 → (𝜃 → 𝜏)) | |
4 | 2, 3 | syl6 35 | . 2 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜏))) |
5 | 1, 4 | mpdd 43 | 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: syl6ci 71 syldd 72 impbidd 209 pm5.21ndd 381 jcad 514 a2and 844 zorn2lem6 10496 sqreulem 15306 ontopbas 35313 ontgval 35316 ordtoplem 35320 ordcmp 35332 fvineqsneu 36292 jaodd 41025 ee33 43282 sb5ALT 43286 tratrb 43297 onfrALTlem2 43307 onfrALT 43310 ax6e2ndeq 43320 ee22an 43434 sspwtrALT 43583 sspwtrALT2 43584 trintALT 43642 |
Copyright terms: Public domain | W3C validator |