![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > syl323anc | 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 | ⊢ (𝜑 → 𝜌) |
syl323anc.9 | ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎 ∧ 𝜌)) → 𝜇) |
Ref | Expression |
---|---|
syl323anc | ⊢ (𝜑 → 𝜇) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl3anc.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | syl3anc.2 | . 2 ⊢ (𝜑 → 𝜒) | |
3 | syl3anc.3 | . 2 ⊢ (𝜑 → 𝜃) | |
4 | syl3Xanc.4 | . . 3 ⊢ (𝜑 → 𝜏) | |
5 | syl23anc.5 | . . 3 ⊢ (𝜑 → 𝜂) | |
6 | 4, 5 | jca 512 | . 2 ⊢ (𝜑 → (𝜏 ∧ 𝜂)) |
7 | syl33anc.6 | . 2 ⊢ (𝜑 → 𝜁) | |
8 | syl133anc.7 | . 2 ⊢ (𝜑 → 𝜎) | |
9 | syl233anc.8 | . 2 ⊢ (𝜑 → 𝜌) | |
10 | syl323anc.9 | . 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎 ∧ 𝜌)) → 𝜇) | |
11 | 1, 2, 3, 6, 7, 8, 9, 10 | syl313anc 1394 | 1 ⊢ (𝜑 → 𝜇) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1087 |
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 206 df-an 397 df-3an 1089 |
This theorem is referenced by: 4atlem11 38566 dalem52 38681 dath2 38694 dalawlem1 38828 dalaw 38843 cdlemb2 38998 4atexlem7 39032 cdleme7ga 39205 cdleme18a 39248 cdleme18c 39250 cdleme21f 39289 cdleme26f2ALTN 39321 cdleme26f2 39322 cdleme27a 39324 cdlemg17dN 39620 cdlemg18a 39635 cdlemg31d 39657 cdlemg48 39694 cdlemj1 39778 dihord4 40215 |
Copyright terms: Public domain | W3C validator |