|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > syl332anc | 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 | ⊢ (𝜑 → 𝜁) | 
| syl133anc.7 | ⊢ (𝜑 → 𝜎) | 
| syl233anc.8 | ⊢ (𝜑 → 𝜌) | 
| syl332anc.9 | ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ (𝜎 ∧ 𝜌)) → 𝜇) | 
| Ref | Expression | 
|---|---|
| syl332anc | ⊢ (𝜑 → 𝜇) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | syl3anc.1 | . 2 ⊢ (𝜑 → 𝜓) | |
| 2 | syl3anc.2 | . 2 ⊢ (𝜑 → 𝜒) | |
| 3 | syl3anc.3 | . 2 ⊢ (𝜑 → 𝜃) | |
| 4 | syl3Xanc.4 | . 2 ⊢ (𝜑 → 𝜏) | |
| 5 | syl23anc.5 | . 2 ⊢ (𝜑 → 𝜂) | |
| 6 | syl33anc.6 | . 2 ⊢ (𝜑 → 𝜁) | |
| 7 | syl133anc.7 | . . 3 ⊢ (𝜑 → 𝜎) | |
| 8 | syl233anc.8 | . . 3 ⊢ (𝜑 → 𝜌) | |
| 9 | 7, 8 | jca 511 | . 2 ⊢ (𝜑 → (𝜎 ∧ 𝜌)) | 
| 10 | syl332anc.9 | . 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ (𝜎 ∧ 𝜌)) → 𝜇) | |
| 11 | 1, 2, 3, 4, 5, 6, 9, 10 | syl331anc 1396 | 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: mdetunilem5 22623 mdetuni0 22628 lnjatN 39783 lncmp 39786 cdlema1N 39794 4atexlemex6 40077 cdlemd4 40204 cdleme18c 40296 cdleme18d 40298 cdleme19b 40307 cdleme21ct 40332 cdleme21d 40333 cdleme21e 40334 cdleme21k 40341 cdleme22g 40351 cdleme24 40355 cdleme27a 40370 cdleme27N 40372 cdleme28a 40373 cdleme40n 40471 cdlemg16zz 40663 cdlemg37 40692 cdlemk21-2N 40894 cdlemk20-2N 40895 cdlemk28-3 40911 cdlemk19xlem 40945 | 
| Copyright terms: Public domain | W3C validator |