Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > syl322anc | Structured version Visualization version GIF version |
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
Ref | Expression |
---|---|
syl12anc.1 | ⊢ (𝜑 → 𝜓) |
syl12anc.2 | ⊢ (𝜑 → 𝜒) |
syl12anc.3 | ⊢ (𝜑 → 𝜃) |
syl22anc.4 | ⊢ (𝜑 → 𝜏) |
syl23anc.5 | ⊢ (𝜑 → 𝜂) |
syl33anc.6 | ⊢ (𝜑 → 𝜁) |
syl133anc.7 | ⊢ (𝜑 → 𝜎) |
syl322anc.8 | ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎)) → 𝜌) |
Ref | Expression |
---|---|
syl322anc | ⊢ (𝜑 → 𝜌) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl12anc.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | syl12anc.2 | . 2 ⊢ (𝜑 → 𝜒) | |
3 | syl12anc.3 | . 2 ⊢ (𝜑 → 𝜃) | |
4 | syl22anc.4 | . 2 ⊢ (𝜑 → 𝜏) | |
5 | syl23anc.5 | . 2 ⊢ (𝜑 → 𝜂) | |
6 | syl33anc.6 | . . 3 ⊢ (𝜑 → 𝜁) | |
7 | syl133anc.7 | . . 3 ⊢ (𝜑 → 𝜎) | |
8 | 6, 7 | jca 553 | . 2 ⊢ (𝜑 → (𝜁 ∧ 𝜎)) |
9 | syl322anc.8 | . 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎)) → 𝜌) | |
10 | 1, 2, 3, 4, 5, 8, 9 | syl321anc 1340 | 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: ax5seglem6 25614 ax5seg 25618 elpaddatriN 34107 paddasslem8 34131 paddasslem12 34135 paddasslem13 34136 pmodlem1 34150 osumcllem5N 34264 pexmidlem2N 34275 cdleme3h 34540 cdleme7ga 34553 cdleme20l 34628 cdleme21ct 34635 cdleme21d 34636 cdleme21e 34637 cdleme26e 34665 cdleme26eALTN 34667 cdleme26fALTN 34668 cdleme26f 34669 cdleme26f2ALTN 34670 cdleme26f2 34671 cdleme39n 34772 cdlemh2 35122 cdlemh 35123 cdlemk12 35156 cdlemk12u 35178 cdlemkfid1N 35227 congsub 36555 mzpcong 36557 jm2.18 36573 jm2.15nn0 36588 jm2.27c 36592 |
Copyright terms: Public domain | W3C validator |