![]() |
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 378 jcad 511 a2and 843 zorn2lem6 10544 sqreulem 15364 ontopbas 36140 ontgval 36143 ordtoplem 36147 ordcmp 36159 fvineqsneu 37118 jaodd 41931 ee33 44197 sb5ALT 44201 tratrb 44212 onfrALTlem2 44222 onfrALT 44225 ax6e2ndeq 44235 ee22an 44349 sspwtrALT 44498 sspwtrALT2 44499 trintALT 44557 |
Copyright terms: Public domain | W3C validator |