![]() |
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 515 | . 2 ⊢ (𝜑 → (𝜎 ∧ 𝜌)) |
10 | syl332anc.9 | . 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ (𝜎 ∧ 𝜌)) → 𝜇) | |
11 | 1, 2, 3, 4, 5, 6, 9, 10 | syl331anc 1392 | 1 ⊢ (𝜑 → 𝜇) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1084 |
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 210 df-an 400 df-3an 1086 |
This theorem is referenced by: mdetunilem5 21221 mdetuni0 21226 lnjatN 37076 lncmp 37079 cdlema1N 37087 4atexlemex6 37370 cdlemd4 37497 cdleme18c 37589 cdleme18d 37591 cdleme19b 37600 cdleme21ct 37625 cdleme21d 37626 cdleme21e 37627 cdleme21k 37634 cdleme22g 37644 cdleme24 37648 cdleme27a 37663 cdleme27N 37665 cdleme28a 37666 cdleme40n 37764 cdlemg16zz 37956 cdlemg37 37985 cdlemk21-2N 38187 cdlemk20-2N 38188 cdlemk28-3 38204 cdlemk19xlem 38238 |
Copyright terms: Public domain | W3C validator |