![]() |
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 511 | . 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 1393 | 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 206 df-an 396 df-3an 1088 |
This theorem is referenced by: 4atlem11 38784 dalem52 38899 dath2 38912 dalawlem1 39046 dalaw 39061 cdlemb2 39216 4atexlem7 39250 cdleme7ga 39423 cdleme18a 39466 cdleme18c 39468 cdleme21f 39507 cdleme26f2ALTN 39539 cdleme26f2 39540 cdleme27a 39542 cdlemg17dN 39838 cdlemg18a 39853 cdlemg31d 39875 cdlemg48 39912 cdlemj1 39996 dihord4 40433 |
Copyright terms: Public domain | W3C validator |