![]() |
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 |
---|---|
syl3anc.1 | ⊢ (𝜑 → 𝜓) |
syl3anc.2 | ⊢ (𝜑 → 𝜒) |
syl3anc.3 | ⊢ (𝜑 → 𝜃) |
syl3Xanc.4 | ⊢ (𝜑 → 𝜏) |
syl23anc.5 | ⊢ (𝜑 → 𝜂) |
syl33anc.6 | ⊢ (𝜑 → 𝜁) |
syl133anc.7 | ⊢ (𝜑 → 𝜎) |
syl322anc.8 | ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎)) → 𝜌) |
Ref | Expression |
---|---|
syl322anc | ⊢ (𝜑 → 𝜌) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl3anc.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | syl3anc.2 | . 2 ⊢ (𝜑 → 𝜒) | |
3 | syl3anc.3 | . 2 ⊢ (𝜑 → 𝜃) | |
4 | syl3Xanc.4 | . 2 ⊢ (𝜑 → 𝜏) | |
5 | syl23anc.5 | . 2 ⊢ (𝜑 → 𝜂) | |
6 | syl33anc.6 | . . 3 ⊢ (𝜑 → 𝜁) | |
7 | syl133anc.7 | . . 3 ⊢ (𝜑 → 𝜎) | |
8 | 6, 7 | jca 513 | . 2 ⊢ (𝜑 → (𝜁 ∧ 𝜎)) |
9 | syl322anc.8 | . 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎)) → 𝜌) | |
10 | 1, 2, 3, 4, 5, 8, 9 | syl321anc 1393 | 1 ⊢ (𝜑 → 𝜌) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∧ w3a 1088 |
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 398 df-3an 1090 |
This theorem is referenced by: cofcut2d 27410 ax5seglem6 28192 ax5seg 28196 elpaddatriN 38674 paddasslem8 38698 paddasslem12 38702 paddasslem13 38703 pmodlem1 38717 osumcllem5N 38831 pexmidlem2N 38842 cdleme3h 39106 cdleme7ga 39119 cdleme20l 39193 cdleme21ct 39200 cdleme21d 39201 cdleme21e 39202 cdleme26e 39230 cdleme26eALTN 39232 cdleme26fALTN 39233 cdleme26f 39234 cdleme26f2ALTN 39235 cdleme26f2 39236 cdleme39n 39337 cdlemh2 39687 cdlemh 39688 cdlemk12 39721 cdlemk12u 39743 cdlemkfid1N 39792 congsub 41709 mzpcong 41711 jm2.18 41727 jm2.15nn0 41742 jm2.27c 41746 |
Copyright terms: Public domain | W3C validator |