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 200 pm5.21ndd 369 jcad 555 zorn2lem6 9323 sqreulem 14099 ontopbas 32427 ontgval 32430 ordtoplem 32434 ordcmp 32446 ee33 38727 sb5ALT 38731 tratrb 38746 onfrALTlem2 38761 onfrALT 38764 ax6e2ndeq 38775 ee22an 38898 sspwtrALT 39049 sspwtrALT2 39058 trintALT 39117 |
Copyright terms: Public domain | W3C validator |