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 |
---|---|
syl12anc.1 | ⊢ (𝜑 → 𝜓) |
syl12anc.2 | ⊢ (𝜑 → 𝜒) |
syl12anc.3 | ⊢ (𝜑 → 𝜃) |
syl22anc.4 | ⊢ (𝜑 → 𝜏) |
syl23anc.5 | ⊢ (𝜑 → 𝜂) |
syl113anc.6 | ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁) |
Ref | Expression |
---|---|
syl113anc | ⊢ (𝜑 → 𝜁) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl12anc.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | syl12anc.2 | . 2 ⊢ (𝜑 → 𝜒) | |
3 | syl12anc.3 | . . 3 ⊢ (𝜑 → 𝜃) | |
4 | syl22anc.4 | . . 3 ⊢ (𝜑 → 𝜏) | |
5 | syl23anc.5 | . . 3 ⊢ (𝜑 → 𝜂) | |
6 | 3, 4, 5 | 3jca 1235 | . 2 ⊢ (𝜑 → (𝜃 ∧ 𝜏 ∧ 𝜂)) |
7 | syl113anc.6 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁) | |
8 | 1, 2, 6, 7 | syl3anc 1318 | 1 ⊢ (𝜑 → 𝜁) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1031 |
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 196 df-an 385 df-3an 1033 |
This theorem is referenced by: syl123anc 1335 syl213anc 1337 pythagtriplem18 15375 initoeu2 16489 psgnunilem1 17736 mulmarep1gsum1 20198 mulmarep1gsum2 20199 smadiadetlem4 20294 cramerimplem2 20309 cramerlem2 20313 cramer 20316 cnhaus 20968 dishaus 20996 ordthauslem 20997 pthaus 21251 txhaus 21260 xkohaus 21266 regr1lem 21352 methaus 22135 metnrmlem3 22472 f1otrge 25552 axpaschlem 25620 n4cyclfrgra 26545 br8d 28802 lt2addrd 28903 xlt2addrd 28913 br8 30899 br4 30901 btwnxfr 31333 lineext 31353 brsegle 31385 brsegle2 31386 lfl0 33370 lfladd 33371 lflsub 33372 lflmul 33373 lflnegcl 33380 lflvscl 33382 lkrlss 33400 3dimlem3 33765 3dimlem4 33768 3dim3 33773 2llnm3N 33873 2lplnja 33923 4atex 34380 4atex3 34385 trlval4 34493 cdleme7c 34550 cdleme7d 34551 cdleme7ga 34553 cdleme21h 34640 cdleme21i 34641 cdleme21j 34642 cdleme21 34643 cdleme32d 34750 cdleme32f 34752 cdleme35h2 34763 cdleme38m 34769 cdleme40m 34773 cdlemg8 34937 cdlemg11a 34943 cdlemg10a 34946 cdlemg12b 34950 cdlemg12d 34952 cdlemg12f 34954 cdlemg12g 34955 cdlemg15a 34961 cdlemg16 34963 cdlemg16z 34965 cdlemg18a 34984 cdlemg24 34994 cdlemg29 35011 cdlemg33b 35013 cdlemg38 35021 cdlemg39 35022 cdlemg40 35023 cdlemg44b 35038 cdlemj2 35128 cdlemk7 35154 cdlemk12 35156 cdlemk12u 35178 cdlemk32 35203 cdlemk25-3 35210 cdlemk34 35216 cdlemkid3N 35239 cdlemkid4 35240 cdlemk11t 35252 cdlemk53 35263 cdlemk55b 35266 cdleml3N 35284 hdmapln1 36216 wwlksnwwlksnon 41121 n4cyclfrgr 41461 |
Copyright terms: Public domain | W3C validator |