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 1235 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) |
5 | syl22anc.4 | . 2 ⊢ (𝜑 → 𝜏) | |
6 | syl23anc.5 | . 2 ⊢ (𝜑 → 𝜂) | |
7 | syl33anc.6 | . 2 ⊢ (𝜑 → 𝜁) | |
8 | syl33anc.7 | . 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁)) → 𝜎) | |
9 | 4, 5, 6, 7, 8 | syl13anc 1320 | 1 ⊢ (𝜑 → 𝜎) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ 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: initoeu2lem2 16488 mdetunilem9 20245 mdetuni0 20246 xmetrtri 21970 bl2in 22015 blhalf 22020 blssps 22039 blss 22040 blcld 22120 methaus 22135 metdstri 22462 metdscnlem 22466 metnrmlem3 22472 xlebnum 22572 pmltpclem1 23024 colinearalglem2 25587 axlowdim 25641 ssbnd 32757 totbndbnd 32758 heiborlem6 32785 2atm 33831 lplncvrlvol2 33919 dalem19 33986 paddasslem9 34132 pclclN 34195 pclfinN 34204 pclfinclN 34254 pexmidlem8N 34281 trlval3 34492 cdleme22b 34647 cdlemefr29bpre0N 34712 cdlemefr29clN 34713 cdlemefr32fvaN 34715 cdlemefr32fva1 34716 cdlemg31b0N 35000 cdlemg31b0a 35001 cdlemh 35123 dihmeetlem16N 35629 dihmeetlem18N 35631 dihmeetlem19N 35632 dihmeetlem20N 35633 hoidmvlelem1 39485 |
Copyright terms: Public domain | W3C validator |