| 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 846 zorn2lem6 10541 sqreulem 15398 ontopbas 36429 ontgval 36432 ordtoplem 36436 ordcmp 36448 fvineqsneu 37412 jaodd 42247 ee33 44541 sb5ALT 44545 tratrb 44556 onfrALTlem2 44566 onfrALT 44569 ax6e2ndeq 44579 ee22an 44693 sspwtrALT 44842 sspwtrALT2 44843 trintALT 44901 |
| Copyright terms: Public domain | W3C validator |