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 514 | . 2 ⊢ (𝜑 → (𝜎 ∧ 𝜌)) |
10 | syl332anc.9 | . 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ (𝜎 ∧ 𝜌)) → 𝜇) | |
11 | 1, 2, 3, 4, 5, 6, 9, 10 | syl331anc 1391 | 1 ⊢ (𝜑 → 𝜇) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 ∧ w3a 1083 |
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 209 df-an 399 df-3an 1085 |
This theorem is referenced by: mdetunilem5 21227 mdetuni0 21232 lnjatN 36918 lncmp 36921 cdlema1N 36929 4atexlemex6 37212 cdlemd4 37339 cdleme18c 37431 cdleme18d 37433 cdleme19b 37442 cdleme21ct 37467 cdleme21d 37468 cdleme21e 37469 cdleme21k 37476 cdleme22g 37486 cdleme24 37490 cdleme27a 37505 cdleme27N 37507 cdleme28a 37508 cdleme40n 37606 cdlemg16zz 37798 cdlemg37 37827 cdlemk21-2N 38029 cdlemk20-2N 38030 cdlemk28-3 38046 cdlemk19xlem 38080 |
Copyright terms: Public domain | W3C validator |