| 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 1129 | . 2 ⊢ (𝜑 → (𝜃 ∧ 𝜏 ∧ 𝜂)) |
| 7 | syl113anc.6 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁) | |
| 8 | 1, 2, 6, 7 | syl3anc 1373 | 1 ⊢ (𝜑 → 𝜁) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ w3a 1087 |
| 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 207 df-an 396 df-3an 1089 |
| This theorem is referenced by: syl123anc 1389 syl213anc 1391 hash7g 14525 pythagtriplem18 16870 initoeu2 18061 psgnunilem1 19511 mulmarep1gsum1 22579 mulmarep1gsum2 22580 smadiadetlem4 22675 cramerimplem2 22690 cramerlem2 22694 cramer 22697 cnhaus 23362 dishaus 23390 ordthauslem 23391 pthaus 23646 txhaus 23655 xkohaus 23661 regr1lem 23747 methaus 24533 metnrmlem3 24883 nosupres 27752 nosupbnd1lem1 27753 nosupbnd2 27761 noinfres 27767 noinfbnd1lem1 27768 iscgrad 28819 f1otrge 28880 axpaschlem 28955 wwlksnwwlksnon 29935 n4cyclfrgr 30310 br8d 32622 lt2addrd 32755 xlt2addrd 32762 br8 35756 br4 35758 btwnxfr 36057 lineext 36077 brsegle 36109 brsegle2 36110 lfl0 39066 lfladd 39067 lflsub 39068 lflmul 39069 lflnegcl 39076 lflvscl 39078 lkrlss 39096 3dimlem3 39463 3dimlem4 39466 3dim3 39471 2llnm3N 39571 2lplnja 39621 4atex 40078 4atex3 40083 trlval4 40190 cdleme7c 40247 cdleme7d 40248 cdleme7ga 40250 cdleme21h 40336 cdleme21i 40337 cdleme21j 40338 cdleme21 40339 cdleme32d 40446 cdleme32f 40448 cdleme35h2 40459 cdleme38m 40465 cdleme40m 40469 cdlemg8 40633 cdlemg11a 40639 cdlemg10a 40642 cdlemg12b 40646 cdlemg12d 40648 cdlemg12f 40650 cdlemg12g 40651 cdlemg15a 40657 cdlemg16 40659 cdlemg16z 40661 cdlemg18a 40680 cdlemg24 40690 cdlemg29 40707 cdlemg33b 40709 cdlemg38 40717 cdlemg39 40718 cdlemg40 40719 cdlemg44b 40734 cdlemj2 40824 cdlemk7 40850 cdlemk12 40852 cdlemk12u 40874 cdlemk32 40899 cdlemk25-3 40906 cdlemk34 40912 cdlemkid3N 40935 cdlemkid4 40936 cdlemk11t 40948 cdlemk53 40959 cdlemk55b 40962 cdleml3N 40980 hdmapln1 41908 tfsconcatrev 43361 isubgr3stgrlem6 47938 sepfsepc 48825 |
| Copyright terms: Public domain | W3C validator |