![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > syl33anc | 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 | ⊢ (𝜑 → 𝜂) |
syl33anc.6 | ⊢ (𝜑 → 𝜁) |
syl33anc.7 | ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁)) → 𝜎) |
Ref | Expression |
---|---|
syl33anc | ⊢ (𝜑 → 𝜎) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl3anc.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | syl3anc.2 | . . 3 ⊢ (𝜑 → 𝜒) | |
3 | syl3anc.3 | . . 3 ⊢ (𝜑 → 𝜃) | |
4 | 1, 2, 3 | 3jca 1125 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) |
5 | syl3Xanc.4 | . 2 ⊢ (𝜑 → 𝜏) | |
6 | syl23anc.5 | . 2 ⊢ (𝜑 → 𝜂) | |
7 | syl33anc.6 | . 2 ⊢ (𝜑 → 𝜁) | |
8 | syl33anc.7 | . 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁)) → 𝜎) | |
9 | 4, 5, 6, 7, 8 | syl13anc 1369 | 1 ⊢ (𝜑 → 𝜎) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ 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: xpord3inddlem 8134 initoeu2lem2 17967 mdetunilem9 22444 mdetuni0 22445 xmetrtri 24183 bl2in 24228 blhalf 24233 blssps 24252 blss 24253 blcld 24336 methaus 24351 metdstri 24689 metdscnlem 24693 metnrmlem3 24699 xlebnum 24813 pmltpclem1 25299 colinearalglem2 28634 axlowdim 28688 ssbnd 37146 totbndbnd 37147 heiborlem6 37174 2atm 38888 lplncvrlvol2 38976 dalem19 39043 paddasslem9 39189 pclclN 39252 pclfinN 39261 pclfinclN 39311 pexmidlem8N 39338 trlval3 39548 cdleme22b 39702 cdlemefr29bpre0N 39767 cdlemefr29clN 39768 cdlemefr32fvaN 39770 cdlemefr32fva1 39771 cdlemg31b0N 40055 cdlemg31b0a 40056 cdlemh 40178 dihmeetlem16N 40683 dihmeetlem18N 40685 dihmeetlem19N 40686 dihmeetlem20N 40687 hoidmvlelem1 45796 |
Copyright terms: Public domain | W3C validator |