|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > syl6com | Structured version Visualization version GIF version | ||
| Description: Syllogism inference with commuted antecedents. (Contributed by NM, 25-May-2005.) | 
| Ref | Expression | 
|---|---|
| syl6com.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) | 
| syl6com.2 | ⊢ (𝜒 → 𝜃) | 
| Ref | Expression | 
|---|---|
| syl6com | ⊢ (𝜓 → (𝜑 → 𝜃)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | syl6com.1 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
| 2 | syl6com.2 | . . 3 ⊢ (𝜒 → 𝜃) | |
| 3 | 1, 2 | syl6 35 | . 2 ⊢ (𝜑 → (𝜓 → 𝜃)) | 
| 4 | 3 | com12 32 | 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: 19.33b 1884 19.36imv 1944 sbequ2 2248 nfeqf2 2381 ax6e 2387 axc16i 2440 mo4 2565 rgen2a 3370 sbccomlem 3868 rspn0 4355 wefrc 5678 elinxp 6036 sorpssuni 7753 sorpssint 7754 ordzsl 7867 limuni3 7874 funcnvuni 7955 funrnex 7979 soxp 8155 frrlem4 8315 wfrlem4OLD 8353 wfrlem12OLD 8361 oaabs 8687 eceqoveq 8863 php3OLD 9262 pssinf 9293 unbnn2 9334 inf0 9662 inf3lem5 9673 tcel 9786 frmin 9790 rankxpsuc 9923 carduni 10022 prdom2 10047 dfac5 10170 cflm 10291 indpi 10948 prlem934 11074 negf1o 11694 xrub 13355 injresinjlem 13827 hashgt12el 14462 hashgt12el2 14463 fi1uzind 14547 swrdwrdsymb 14701 cshwcsh2id 14868 cshwshash 17143 lidrididd 18684 dfgrp2 18981 symgextf1 19440 rngdi 20158 rngdir 20159 gsummoncoe1 22313 basis2 22959 fbdmn0 23843 rusgr1vtxlem 29606 upgrewlkle2 29625 clwwlknun 30132 conngrv2edg 30215 frcond1 30286 4cyclusnfrgr 30312 atcv0eq 32399 dfon2lem9 35793 altopthsn 35963 rankeq1o 36173 bj-cbvalimt 36641 bj-cbveximt 36642 wl-orel12 37513 wl-equsb4 37559 rngoueqz 37948 hbtlem5 43145 ntrk0kbimka 44057 funressnfv 47060 afvco2 47193 ndmaovcl 47220 bgoldbtbndlem4 47800 isubgr3stgrlem4 47941 zlmodzxznm 48419 | 
| Copyright terms: Public domain | W3C validator |