![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > syl113anc | Structured version Visualization version GIF version |
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
Ref | Expression |
---|---|
syl3anc.1 | ⊢ (𝜑 → 𝜓) |
syl3anc.2 | ⊢ (𝜑 → 𝜒) |
syl3anc.3 | ⊢ (𝜑 → 𝜃) |
syl3Xanc.4 | ⊢ (𝜑 → 𝜏) |
syl23anc.5 | ⊢ (𝜑 → 𝜂) |
syl113anc.6 | ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁) |
Ref | Expression |
---|---|
syl113anc | ⊢ (𝜑 → 𝜁) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl3anc.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | syl3anc.2 | . 2 ⊢ (𝜑 → 𝜒) | |
3 | syl3anc.3 | . . 3 ⊢ (𝜑 → 𝜃) | |
4 | syl3Xanc.4 | . . 3 ⊢ (𝜑 → 𝜏) | |
5 | syl23anc.5 | . . 3 ⊢ (𝜑 → 𝜂) | |
6 | 3, 4, 5 | 3jca 1126 | . 2 ⊢ (𝜑 → (𝜃 ∧ 𝜏 ∧ 𝜂)) |
7 | syl113anc.6 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁) | |
8 | 1, 2, 6, 7 | syl3anc 1369 | 1 ⊢ (𝜑 → 𝜁) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1085 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 206 df-an 395 df-3an 1087 |
This theorem is referenced by: syl123anc 1385 syl213anc 1387 pythagtriplem18 16769 initoeu2 17970 psgnunilem1 19402 mulmarep1gsum1 22295 mulmarep1gsum2 22296 smadiadetlem4 22391 cramerimplem2 22406 cramerlem2 22410 cramer 22413 cnhaus 23078 dishaus 23106 ordthauslem 23107 pthaus 23362 txhaus 23371 xkohaus 23377 regr1lem 23463 methaus 24249 metnrmlem3 24597 nosupres 27446 nosupbnd1lem1 27447 nosupbnd2 27455 noinfres 27461 noinfbnd1lem1 27462 iscgrad 28329 f1otrge 28390 axpaschlem 28465 wwlksnwwlksnon 29436 n4cyclfrgr 29811 br8d 32106 lt2addrd 32231 xlt2addrd 32238 br8 35030 br4 35032 btwnxfr 35332 lineext 35352 brsegle 35384 brsegle2 35385 lfl0 38238 lfladd 38239 lflsub 38240 lflmul 38241 lflnegcl 38248 lflvscl 38250 lkrlss 38268 3dimlem3 38635 3dimlem4 38638 3dim3 38643 2llnm3N 38743 2lplnja 38793 4atex 39250 4atex3 39255 trlval4 39362 cdleme7c 39419 cdleme7d 39420 cdleme7ga 39422 cdleme21h 39508 cdleme21i 39509 cdleme21j 39510 cdleme21 39511 cdleme32d 39618 cdleme32f 39620 cdleme35h2 39631 cdleme38m 39637 cdleme40m 39641 cdlemg8 39805 cdlemg11a 39811 cdlemg10a 39814 cdlemg12b 39818 cdlemg12d 39820 cdlemg12f 39822 cdlemg12g 39823 cdlemg15a 39829 cdlemg16 39831 cdlemg16z 39833 cdlemg18a 39852 cdlemg24 39862 cdlemg29 39879 cdlemg33b 39881 cdlemg38 39889 cdlemg39 39890 cdlemg40 39891 cdlemg44b 39906 cdlemj2 39996 cdlemk7 40022 cdlemk12 40024 cdlemk12u 40046 cdlemk32 40071 cdlemk25-3 40078 cdlemk34 40084 cdlemkid3N 40107 cdlemkid4 40108 cdlemk11t 40120 cdlemk53 40131 cdlemk55b 40134 cdleml3N 40152 hdmapln1 41080 tfsconcatrev 42400 sepfsepc 47647 |
Copyright terms: Public domain | W3C validator |