![]() |
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 210 pm5.21ndd 379 jcad 512 a2and 845 zorn2lem6 10539 sqreulem 15395 ontopbas 36411 ontgval 36414 ordtoplem 36418 ordcmp 36430 fvineqsneu 37394 jaodd 42227 ee33 44519 sb5ALT 44523 tratrb 44534 onfrALTlem2 44544 onfrALT 44547 ax6e2ndeq 44557 ee22an 44671 sspwtrALT 44820 sspwtrALT2 44821 trintALT 44879 |
Copyright terms: Public domain | W3C validator |