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 1877 sbequ2 2241 nfeqf2 2388 ax6e 2394 axc16i 2453 mo4 2646 rgen2a 3229 wefrc 5543 elinxp 5884 sorpssuni 7447 sorpssint 7448 ordzsl 7548 limuni3 7555 funcnvuni 7624 funrnex 7646 soxp 7814 wfrlem4 7949 wfrlem12 7957 oaabs 8261 eceqoveq 8392 php3 8692 pssinf 8717 unbnn2 8764 inf0 9073 inf3lem5 9084 tcel 9176 rankxpsuc 9300 carduni 9399 prdom2 9421 dfac5 9543 cflm 9661 indpi 10318 prlem934 10444 negf1o 11059 xrub 12695 injresinjlem 13147 hashgt12el 13773 hashgt12el2 13774 fi1uzind 13845 swrdwrdsymb 14014 cshwcsh2id 14180 cshwshash 16428 lidrididd 17870 dfgrp2 18068 symgextf1 18480 gsummoncoe1 20402 basis2 21489 fbdmn0 22372 rusgr1vtxlem 27297 upgrewlkle2 27316 clwwlknun 27819 conngrv2edg 27902 frcond1 27973 4cyclusnfrgr 27999 atcv0eq 30084 dfon2lem9 32934 trpredrec 32975 frmin 32982 frrlem4 33024 altopthsn 33320 rankeq1o 33530 bj-cbvalimt 33870 bj-cbveximt 33871 wl-orel12 34634 wl-equsb4 34675 rngoueqz 35101 hbtlem5 39608 ntrk0kbimka 40269 funressnfv 43159 afvco2 43256 ndmaovcl 43283 bgoldbtbndlem4 43820 rngdir 44051 zlmodzxznm 44450 |
Copyright terms: Public domain | W3C validator |