![]() |
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 240 2eu6 2653 r19.12OLD 3313 dmcosseq 5967 iss 6028 funopg 6574 limuni3 7828 frxp 8099 wfrlem12OLD 8307 tz7.49 8432 dif1ennnALT 9265 enp1iOLD 9268 frfi 9276 unblem3 9285 isfinite2 9289 iunfi 9328 tcrank 9866 infdif 10191 isf34lem6 10362 axdc3lem4 10435 suplem1pr 11034 uzwo 12882 gsumcom2 19826 cmpsublem 22872 nrmhaus 23299 metrest 24002 finiunmbl 25030 h1datomi 30799 chirredlem1 31608 fnrelpredd 34023 mclsax 34491 lineext 34979 onsucconni 35227 cbveud 36158 sdclem2 36516 heibor1lem 36583 iss2 37119 omabs2 41953 cotrintab 42236 tgblthelfgott 46356 setrec1lem2 47573 |
Copyright terms: Public domain | W3C validator |