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 |
---|---|
syl12anc.1 | ⊢ (𝜑 → 𝜓) |
syl12anc.2 | ⊢ (𝜑 → 𝜒) |
syl12anc.3 | ⊢ (𝜑 → 𝜃) |
syl22anc.4 | ⊢ (𝜑 → 𝜏) |
syl23anc.5 | ⊢ (𝜑 → 𝜂) |
syl33anc.6 | ⊢ (𝜑 → 𝜁) |
syl321anc.7 | ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ 𝜁) → 𝜎) |
Ref | Expression |
---|---|
syl321anc | ⊢ (𝜑 → 𝜎) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl12anc.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | syl12anc.2 | . 2 ⊢ (𝜑 → 𝜒) | |
3 | syl12anc.3 | . 2 ⊢ (𝜑 → 𝜃) | |
4 | syl22anc.4 | . . 3 ⊢ (𝜑 → 𝜏) | |
5 | syl23anc.5 | . . 3 ⊢ (𝜑 → 𝜂) | |
6 | 4, 5 | jca 553 | . 2 ⊢ (𝜑 → (𝜏 ∧ 𝜂)) |
7 | syl33anc.6 | . 2 ⊢ (𝜑 → 𝜁) | |
8 | syl321anc.7 | . 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ 𝜁) → 𝜎) | |
9 | 1, 2, 3, 6, 7, 8 | syl311anc 1332 | 1 ⊢ (𝜑 → 𝜎) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1031 |
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 196 df-an 385 df-3an 1033 |
This theorem is referenced by: syl322anc 1346 cxple2ad 24271 chordthmlem3 24361 4noncolr2 33758 4noncolr1 33759 3atlem5 33791 2lplnj 33924 llnmod2i2 34167 dalawlem11 34185 dalawlem12 34186 cdleme43dN 34798 cdleme4gfv 34813 cdlemeg46nlpq 34823 cdlemg17bq 34979 cdlemg31b0N 35000 cdlemg31b0a 35001 cdlemg31c 35005 cdlemg39 35022 cdlemk47 35255 lincext3 42039 |
Copyright terms: Public domain | W3C validator |