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 211 pm5.21ndd 381 jcad 513 a2and 839 zorn2lem6 9911 sqreulem 14707 ontopbas 33673 ontgval 33676 ordtoplem 33680 ordcmp 33692 fvineqsneu 34574 jaodd 38979 ee33 40732 sb5ALT 40736 tratrb 40747 onfrALTlem2 40757 onfrALT 40760 ax6e2ndeq 40770 ee22an 40884 sspwtrALT 41033 sspwtrALT2 41034 trintALT 41092 |
Copyright terms: Public domain | W3C validator |