![]() |
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 1164 | . 2 ⊢ (𝜑 → (𝜃 ∧ 𝜏 ∧ 𝜂)) |
7 | syl113anc.6 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁) | |
8 | 1, 2, 6, 7 | syl3anc 1496 | 1 ⊢ (𝜑 → 𝜁) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1113 |
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 199 df-an 387 df-3an 1115 |
This theorem is referenced by: syl123anc 1512 syl213anc 1514 pythagtriplem18 15907 initoeu2 17017 psgnunilem1 18262 mulmarep1gsum1 20746 mulmarep1gsum2 20747 smadiadetlem4 20843 cramerimplem2 20859 cramerlem2 20863 cramer 20866 cnhaus 21528 dishaus 21556 ordthauslem 21557 pthaus 21811 txhaus 21820 xkohaus 21826 regr1lem 21912 methaus 22694 metnrmlem3 23033 f1otrge 26170 axpaschlem 26238 wwlksnwwlksnon 27243 n4cyclfrgr 27671 br8d 29968 lt2addrd 30062 xlt2addrd 30069 br8 32187 br4 32189 nosupres 32391 nosupbnd1lem1 32392 nosupbnd2 32400 btwnxfr 32701 lineext 32721 brsegle 32753 brsegle2 32754 lfl0 35139 lfladd 35140 lflsub 35141 lflmul 35142 lflnegcl 35149 lflvscl 35151 lkrlss 35169 3dimlem3 35535 3dimlem4 35538 3dim3 35543 2llnm3N 35643 2lplnja 35693 4atex 36150 4atex3 36155 trlval4 36262 cdleme7c 36319 cdleme7d 36320 cdleme7ga 36322 cdleme21h 36408 cdleme21i 36409 cdleme21j 36410 cdleme21 36411 cdleme32d 36518 cdleme32f 36520 cdleme35h2 36531 cdleme38m 36537 cdleme40m 36541 cdlemg8 36705 cdlemg11a 36711 cdlemg10a 36714 cdlemg12b 36718 cdlemg12d 36720 cdlemg12f 36722 cdlemg12g 36723 cdlemg15a 36729 cdlemg16 36731 cdlemg16z 36733 cdlemg18a 36752 cdlemg24 36762 cdlemg29 36779 cdlemg33b 36781 cdlemg38 36789 cdlemg39 36790 cdlemg40 36791 cdlemg44b 36806 cdlemj2 36896 cdlemk7 36922 cdlemk12 36924 cdlemk12u 36946 cdlemk32 36971 cdlemk25-3 36978 cdlemk34 36984 cdlemkid3N 37007 cdlemkid4 37008 cdlemk11t 37020 cdlemk53 37031 cdlemk55b 37034 cdleml3N 37052 hdmapln1 37980 |
Copyright terms: Public domain | W3C validator |