![]() |
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 |
---|---|
syl12anc.1 | ⊢ (𝜑 → 𝜓) |
syl12anc.2 | ⊢ (𝜑 → 𝜒) |
syl12anc.3 | ⊢ (𝜑 → 𝜃) |
syl22anc.4 | ⊢ (𝜑 → 𝜏) |
syl23anc.5 | ⊢ (𝜑 → 𝜂) |
syl33anc.6 | ⊢ (𝜑 → 𝜁) |
syl133anc.7 | ⊢ (𝜑 → 𝜎) |
syl233anc.8 | ⊢ (𝜑 → 𝜌) |
syl332anc.9 | ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ (𝜎 ∧ 𝜌)) → 𝜇) |
Ref | Expression |
---|---|
syl332anc | ⊢ (𝜑 → 𝜇) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl12anc.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | syl12anc.2 | . 2 ⊢ (𝜑 → 𝜒) | |
3 | syl12anc.3 | . 2 ⊢ (𝜑 → 𝜃) | |
4 | syl22anc.4 | . 2 ⊢ (𝜑 → 𝜏) | |
5 | syl23anc.5 | . 2 ⊢ (𝜑 → 𝜂) | |
6 | syl33anc.6 | . 2 ⊢ (𝜑 → 𝜁) | |
7 | syl133anc.7 | . . 3 ⊢ (𝜑 → 𝜎) | |
8 | syl233anc.8 | . . 3 ⊢ (𝜑 → 𝜌) | |
9 | 7, 8 | jca 501 | . 2 ⊢ (𝜑 → (𝜎 ∧ 𝜌)) |
10 | syl332anc.9 | . 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ (𝜎 ∧ 𝜌)) → 𝜇) | |
11 | 1, 2, 3, 4, 5, 6, 9, 10 | syl331anc 1501 | 1 ⊢ (𝜑 → 𝜇) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 382 ∧ w3a 1071 |
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 383 df-3an 1073 |
This theorem is referenced by: mdetunilem5 20640 mdetuni0 20645 lnjatN 35588 lncmp 35591 cdlema1N 35599 4atexlemex6 35882 cdlemd4 36010 cdleme18c 36102 cdleme18d 36104 cdleme19b 36113 cdleme21ct 36138 cdleme21d 36139 cdleme21e 36140 cdleme21k 36147 cdleme22g 36157 cdleme24 36161 cdleme27a 36176 cdleme27N 36178 cdleme28a 36179 cdleme40n 36277 cdlemg16zz 36469 cdlemg37 36498 cdlemk21-2N 36700 cdlemk20-2N 36701 cdlemk28-3 36717 cdlemk19xlem 36751 |
Copyright terms: Public domain | W3C validator |