![]() |
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 1127 | . 2 ⊢ (𝜑 → (𝜃 ∧ 𝜏 ∧ 𝜂)) |
7 | syl113anc.6 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁) | |
8 | 1, 2, 6, 7 | syl3anc 1370 | 1 ⊢ (𝜑 → 𝜁) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1086 |
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 396 df-3an 1088 |
This theorem is referenced by: syl123anc 1386 syl213anc 1388 pythagtriplem18 16770 initoeu2 17971 psgnunilem1 19403 mulmarep1gsum1 22296 mulmarep1gsum2 22297 smadiadetlem4 22392 cramerimplem2 22407 cramerlem2 22411 cramer 22414 cnhaus 23079 dishaus 23107 ordthauslem 23108 pthaus 23363 txhaus 23372 xkohaus 23378 regr1lem 23464 methaus 24250 metnrmlem3 24598 nosupres 27447 nosupbnd1lem1 27448 nosupbnd2 27456 noinfres 27462 noinfbnd1lem1 27463 iscgrad 28330 f1otrge 28391 axpaschlem 28466 wwlksnwwlksnon 29437 n4cyclfrgr 29812 br8d 32107 lt2addrd 32232 xlt2addrd 32239 br8 35031 br4 35033 btwnxfr 35333 lineext 35353 brsegle 35385 brsegle2 35386 lfl0 38239 lfladd 38240 lflsub 38241 lflmul 38242 lflnegcl 38249 lflvscl 38251 lkrlss 38269 3dimlem3 38636 3dimlem4 38639 3dim3 38644 2llnm3N 38744 2lplnja 38794 4atex 39251 4atex3 39256 trlval4 39363 cdleme7c 39420 cdleme7d 39421 cdleme7ga 39423 cdleme21h 39509 cdleme21i 39510 cdleme21j 39511 cdleme21 39512 cdleme32d 39619 cdleme32f 39621 cdleme35h2 39632 cdleme38m 39638 cdleme40m 39642 cdlemg8 39806 cdlemg11a 39812 cdlemg10a 39815 cdlemg12b 39819 cdlemg12d 39821 cdlemg12f 39823 cdlemg12g 39824 cdlemg15a 39830 cdlemg16 39832 cdlemg16z 39834 cdlemg18a 39853 cdlemg24 39863 cdlemg29 39880 cdlemg33b 39882 cdlemg38 39890 cdlemg39 39891 cdlemg40 39892 cdlemg44b 39907 cdlemj2 39997 cdlemk7 40023 cdlemk12 40025 cdlemk12u 40047 cdlemk32 40072 cdlemk25-3 40079 cdlemk34 40085 cdlemkid3N 40108 cdlemkid4 40109 cdlemk11t 40121 cdlemk53 40132 cdlemk55b 40135 cdleml3N 40153 hdmapln1 41081 tfsconcatrev 42401 sepfsepc 47648 |
Copyright terms: Public domain | W3C validator |