| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > sylcom | Structured version Visualization version GIF version | ||
| Description: Syllogism inference with commutation of antecedents. (Contributed by NM, 29-Aug-2004.) (Proof shortened by Mel L. O'Cat, 2-Feb-2006.) (Proof shortened by Stefan Allan, 23-Feb-2006.) |
| Ref | Expression |
|---|---|
| sylcom.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
| sylcom.2 | ⊢ (𝜓 → (𝜒 → 𝜃)) |
| Ref | Expression |
|---|---|
| sylcom | ⊢ (𝜑 → (𝜓 → 𝜃)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sylcom.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
| 2 | sylcom.2 | . . 3 ⊢ (𝜓 → (𝜒 → 𝜃)) | |
| 3 | 2 | a2i 14 | . 2 ⊢ ((𝜓 → 𝜒) → (𝜓 → 𝜃)) |
| 4 | 1, 3 | syl 17 | 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: syl5com 31 syl6 35 syli 39 pm2.18d 127 mpbidi 241 2eu6 2657 r19.12OLD 3315 dmcosseq 5987 dmcosseqOLD 5988 iss 6053 funopg 6600 limuni3 7873 frxp 8151 wfrlem12OLD 8360 tz7.49 8485 dif1ennnALT 9311 enp1iOLD 9314 frfi 9321 unblem3 9330 isfinite2 9334 iunfi 9383 tcrank 9924 infdif 10248 isf34lem6 10420 axdc3lem4 10493 suplem1pr 11092 uzwo 12953 gsumcom2 19993 cmpsublem 23407 nrmhaus 23834 metrest 24537 finiunmbl 25579 h1datomi 31600 chirredlem1 32409 fnrelpredd 35103 mclsax 35574 lineext 36077 in-ax8 36225 ss-ax8 36226 onsucconni 36438 cbveud 37373 sdclem2 37749 heibor1lem 37816 iss2 38345 omabs2 43345 cotrintab 43627 tgblthelfgott 47802 setrec1lem2 49207 |
| Copyright terms: Public domain | W3C validator |