|   | 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 1128 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) | 
| 5 | syl3Xanc.4 | . 2 ⊢ (𝜑 → 𝜏) | |
| 6 | syl23anc.5 | . 2 ⊢ (𝜑 → 𝜂) | |
| 7 | syl33anc.6 | . 2 ⊢ (𝜑 → 𝜁) | |
| 8 | syl33anc.7 | . 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁)) → 𝜎) | |
| 9 | 4, 5, 6, 7, 8 | syl13anc 1373 | 1 ⊢ (𝜑 → 𝜎) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 | 
| 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 207 df-an 396 df-3an 1088 | 
| This theorem is referenced by: xpord3inddlem 8180 initoeu2lem2 18061 mdetunilem9 22627 mdetuni0 22628 xmetrtri 24366 bl2in 24411 blhalf 24416 blssps 24435 blss 24436 blcld 24519 methaus 24534 metdstri 24874 metdscnlem 24878 metnrmlem3 24884 xlebnum 24998 pmltpclem1 25484 colinearalglem2 28923 axlowdim 28977 ssbnd 37796 totbndbnd 37797 heiborlem6 37824 2atm 39530 lplncvrlvol2 39618 dalem19 39685 paddasslem9 39831 pclclN 39894 pclfinN 39903 pclfinclN 39953 pexmidlem8N 39980 trlval3 40190 cdleme22b 40344 cdlemefr29bpre0N 40409 cdlemefr29clN 40410 cdlemefr32fvaN 40412 cdlemefr32fva1 40413 cdlemg31b0N 40697 cdlemg31b0a 40698 cdlemh 40820 dihmeetlem16N 41325 dihmeetlem18N 41327 dihmeetlem19N 41328 dihmeetlem20N 41329 hoidmvlelem1 46615 | 
| Copyright terms: Public domain | W3C validator |