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 |
---|---|
syl12anc.1 | ⊢ (𝜑 → 𝜓) |
syl12anc.2 | ⊢ (𝜑 → 𝜒) |
syl12anc.3 | ⊢ (𝜑 → 𝜃) |
syl22anc.4 | ⊢ (𝜑 → 𝜏) |
syl23anc.5 | ⊢ (𝜑 → 𝜂) |
syl33anc.6 | ⊢ (𝜑 → 𝜁) |
syl33anc.7 | ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁)) → 𝜎) |
Ref | Expression |
---|---|
syl33anc | ⊢ (𝜑 → 𝜎) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl12anc.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | syl12anc.2 | . . 3 ⊢ (𝜑 → 𝜒) | |
3 | syl12anc.3 | . . 3 ⊢ (𝜑 → 𝜃) | |
4 | 1, 2, 3 | 3jca 1242 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) |
5 | syl22anc.4 | . 2 ⊢ (𝜑 → 𝜏) | |
6 | syl23anc.5 | . 2 ⊢ (𝜑 → 𝜂) | |
7 | syl33anc.6 | . 2 ⊢ (𝜑 → 𝜁) | |
8 | syl33anc.7 | . 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁)) → 𝜎) | |
9 | 4, 5, 6, 7, 8 | syl13anc 1328 | 1 ⊢ (𝜑 → 𝜎) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 384 ∧ 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: initoeu2lem2 16665 mdetunilem9 20426 mdetuni0 20427 xmetrtri 22160 bl2in 22205 blhalf 22210 blssps 22229 blss 22230 blcld 22310 methaus 22325 metdstri 22654 metdscnlem 22658 metnrmlem3 22664 xlebnum 22764 pmltpclem1 23217 colinearalglem2 25787 axlowdim 25841 ssbnd 33587 totbndbnd 33588 heiborlem6 33615 2atm 34813 lplncvrlvol2 34901 dalem19 34968 paddasslem9 35114 pclclN 35177 pclfinN 35186 pclfinclN 35236 pexmidlem8N 35263 trlval3 35474 cdleme22b 35629 cdlemefr29bpre0N 35694 cdlemefr29clN 35695 cdlemefr32fvaN 35697 cdlemefr32fva1 35698 cdlemg31b0N 35982 cdlemg31b0a 35983 cdlemh 36105 dihmeetlem16N 36611 dihmeetlem18N 36613 dihmeetlem19N 36614 dihmeetlem20N 36615 hoidmvlelem1 40809 |
Copyright terms: Public domain | W3C validator |