![]() |
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 1125 | . 2 ⊢ (𝜑 → (𝜃 ∧ 𝜏 ∧ 𝜂)) |
7 | syl113anc.6 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁) | |
8 | 1, 2, 6, 7 | syl3anc 1368 | 1 ⊢ (𝜑 → 𝜁) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1084 |
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 1086 |
This theorem is referenced by: syl123anc 1384 syl213anc 1386 pythagtriplem18 16764 initoeu2 17968 psgnunilem1 19403 mulmarep1gsum1 22397 mulmarep1gsum2 22398 smadiadetlem4 22493 cramerimplem2 22508 cramerlem2 22512 cramer 22515 cnhaus 23180 dishaus 23208 ordthauslem 23209 pthaus 23464 txhaus 23473 xkohaus 23479 regr1lem 23565 methaus 24351 metnrmlem3 24699 nosupres 27556 nosupbnd1lem1 27557 nosupbnd2 27565 noinfres 27571 noinfbnd1lem1 27572 iscgrad 28531 f1otrge 28592 axpaschlem 28667 wwlksnwwlksnon 29638 n4cyclfrgr 30013 br8d 32308 lt2addrd 32433 xlt2addrd 32440 br8 35221 br4 35223 btwnxfr 35523 lineext 35543 brsegle 35575 brsegle2 35576 lfl0 38425 lfladd 38426 lflsub 38427 lflmul 38428 lflnegcl 38435 lflvscl 38437 lkrlss 38455 3dimlem3 38822 3dimlem4 38825 3dim3 38830 2llnm3N 38930 2lplnja 38980 4atex 39437 4atex3 39442 trlval4 39549 cdleme7c 39606 cdleme7d 39607 cdleme7ga 39609 cdleme21h 39695 cdleme21i 39696 cdleme21j 39697 cdleme21 39698 cdleme32d 39805 cdleme32f 39807 cdleme35h2 39818 cdleme38m 39824 cdleme40m 39828 cdlemg8 39992 cdlemg11a 39998 cdlemg10a 40001 cdlemg12b 40005 cdlemg12d 40007 cdlemg12f 40009 cdlemg12g 40010 cdlemg15a 40016 cdlemg16 40018 cdlemg16z 40020 cdlemg18a 40039 cdlemg24 40049 cdlemg29 40066 cdlemg33b 40068 cdlemg38 40076 cdlemg39 40077 cdlemg40 40078 cdlemg44b 40093 cdlemj2 40183 cdlemk7 40209 cdlemk12 40211 cdlemk12u 40233 cdlemk32 40258 cdlemk25-3 40265 cdlemk34 40271 cdlemkid3N 40294 cdlemkid4 40295 cdlemk11t 40307 cdlemk53 40318 cdlemk55b 40321 cdleml3N 40339 hdmapln1 41267 tfsconcatrev 42587 sepfsepc 47748 |
Copyright terms: Public domain | W3C validator |