![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > syl321anc | Structured version Visualization version GIF version |
Description: Syllogism combined with contraction. (Contributed by NM, 11-Jul-2012.) |
Ref | Expression |
---|---|
syl3anc.1 | ⊢ (𝜑 → 𝜓) |
syl3anc.2 | ⊢ (𝜑 → 𝜒) |
syl3anc.3 | ⊢ (𝜑 → 𝜃) |
syl3Xanc.4 | ⊢ (𝜑 → 𝜏) |
syl23anc.5 | ⊢ (𝜑 → 𝜂) |
syl33anc.6 | ⊢ (𝜑 → 𝜁) |
syl321anc.7 | ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ 𝜁) → 𝜎) |
Ref | Expression |
---|---|
syl321anc | ⊢ (𝜑 → 𝜎) |
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 | syl321anc.7 | . 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ 𝜁) → 𝜎) | |
9 | 1, 2, 3, 6, 7, 8 | syl311anc 1384 | 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: syl322anc 1398 cxple2ad 26240 chordthmlem3 26346 nosupbnd1lem3 27220 nosupbnd1lem4 27221 noinfbnd1lem3 27235 noinfbnd1lem4 27236 4noncolr2 38411 4noncolr1 38412 3atlem5 38444 2lplnj 38577 llnmod2i2 38820 dalawlem11 38838 dalawlem12 38839 cdleme43dN 39449 cdleme4gfv 39464 cdlemeg46nlpq 39474 cdlemg17bq 39630 cdlemg31b0N 39651 cdlemg31b0a 39652 cdlemg31c 39656 cdlemg39 39673 cdlemk47 39906 lincext3 47215 |
Copyright terms: Public domain | W3C validator |