![]() |
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 1164 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) |
5 | syl3Xanc.4 | . 2 ⊢ (𝜑 → 𝜏) | |
6 | syl23anc.5 | . 2 ⊢ (𝜑 → 𝜂) | |
7 | syl33anc.6 | . 2 ⊢ (𝜑 → 𝜁) | |
8 | syl33anc.7 | . 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁)) → 𝜎) | |
9 | 4, 5, 6, 7, 8 | syl13anc 1497 | 1 ⊢ (𝜑 → 𝜎) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∧ 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: initoeu2lem2 17017 mdetunilem9 20794 mdetuni0 20795 xmetrtri 22530 bl2in 22575 blhalf 22580 blssps 22599 blss 22600 blcld 22680 methaus 22695 metdstri 23024 metdscnlem 23028 metnrmlem3 23034 xlebnum 23134 pmltpclem1 23614 colinearalglem2 26206 axlowdim 26260 ssbnd 34129 totbndbnd 34130 heiborlem6 34157 2atm 35602 lplncvrlvol2 35690 dalem19 35757 paddasslem9 35903 pclclN 35966 pclfinN 35975 pclfinclN 36025 pexmidlem8N 36052 trlval3 36262 cdleme22b 36416 cdlemefr29bpre0N 36481 cdlemefr29clN 36482 cdlemefr32fvaN 36484 cdlemefr32fva1 36485 cdlemg31b0N 36769 cdlemg31b0a 36770 cdlemh 36892 dihmeetlem16N 37397 dihmeetlem18N 37399 dihmeetlem19N 37400 dihmeetlem20N 37401 hoidmvlelem1 41603 |
Copyright terms: Public domain | W3C validator |