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 514 | . 2 ⊢ (𝜑 → (𝜏 ∧ 𝜂)) |
7 | syl33anc.6 | . 2 ⊢ (𝜑 → 𝜁) | |
8 | syl321anc.7 | . 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ 𝜁) → 𝜎) | |
9 | 1, 2, 3, 6, 7, 8 | syl311anc 1380 | 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: syl322anc 1394 cxple2ad 25307 chordthmlem3 25411 nosupbnd1lem3 33210 nosupbnd1lem4 33211 4noncolr2 36589 4noncolr1 36590 3atlem5 36622 2lplnj 36755 llnmod2i2 36998 dalawlem11 37016 dalawlem12 37017 cdleme43dN 37627 cdleme4gfv 37642 cdlemeg46nlpq 37652 cdlemg17bq 37808 cdlemg31b0N 37829 cdlemg31b0a 37830 cdlemg31c 37834 cdlemg39 37851 cdlemk47 38084 lincext3 44510 |
Copyright terms: Public domain | W3C validator |