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 1242 | . 2 ⊢ (𝜑 → (𝜃 ∧ 𝜏 ∧ 𝜂)) |
7 | syl113anc.6 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁) | |
8 | 1, 2, 6, 7 | syl3anc 1326 | 1 ⊢ (𝜑 → 𝜁) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1037 |
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 197 df-an 386 df-3an 1039 |
This theorem is referenced by: syl123anc 1343 syl213anc 1345 pythagtriplem18 15537 initoeu2 16666 psgnunilem1 17913 mulmarep1gsum1 20379 mulmarep1gsum2 20380 smadiadetlem4 20475 cramerimplem2 20490 cramerlem2 20494 cramer 20497 cnhaus 21158 dishaus 21186 ordthauslem 21187 pthaus 21441 txhaus 21450 xkohaus 21456 regr1lem 21542 methaus 22325 metnrmlem3 22664 f1otrge 25752 axpaschlem 25820 wwlksnwwlksnon 26810 n4cyclfrgr 27155 br8d 29422 lt2addrd 29516 xlt2addrd 29523 br8 31646 br4 31648 nosupres 31853 nosupbnd1lem1 31854 nosupbnd2 31862 btwnxfr 32163 lineext 32183 brsegle 32215 brsegle2 32216 lfl0 34352 lfladd 34353 lflsub 34354 lflmul 34355 lflnegcl 34362 lflvscl 34364 lkrlss 34382 3dimlem3 34747 3dimlem4 34750 3dim3 34755 2llnm3N 34855 2lplnja 34905 4atex 35362 4atex3 35367 trlval4 35475 cdleme7c 35532 cdleme7d 35533 cdleme7ga 35535 cdleme21h 35622 cdleme21i 35623 cdleme21j 35624 cdleme21 35625 cdleme32d 35732 cdleme32f 35734 cdleme35h2 35745 cdleme38m 35751 cdleme40m 35755 cdlemg8 35919 cdlemg11a 35925 cdlemg10a 35928 cdlemg12b 35932 cdlemg12d 35934 cdlemg12f 35936 cdlemg12g 35937 cdlemg15a 35943 cdlemg16 35945 cdlemg16z 35947 cdlemg18a 35966 cdlemg24 35976 cdlemg29 35993 cdlemg33b 35995 cdlemg38 36003 cdlemg39 36004 cdlemg40 36005 cdlemg44b 36020 cdlemj2 36110 cdlemk7 36136 cdlemk12 36138 cdlemk12u 36160 cdlemk32 36185 cdlemk25-3 36192 cdlemk34 36198 cdlemkid3N 36221 cdlemkid4 36222 cdlemk11t 36234 cdlemk53 36245 cdlemk55b 36248 cdleml3N 36266 hdmapln1 37198 |
Copyright terms: Public domain | W3C validator |