![]() |
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 515 | . 2 ⊢ (𝜑 → (𝜁 ∧ 𝜎)) |
9 | syl322anc.8 | . 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎)) → 𝜌) | |
10 | 1, 2, 3, 4, 5, 8, 9 | syl321anc 1389 | 1 ⊢ (𝜑 → 𝜌) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1084 |
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 210 df-an 400 df-3an 1086 |
This theorem is referenced by: ax5seglem6 26728 ax5seg 26732 elpaddatriN 37099 paddasslem8 37123 paddasslem12 37127 paddasslem13 37128 pmodlem1 37142 osumcllem5N 37256 pexmidlem2N 37267 cdleme3h 37531 cdleme7ga 37544 cdleme20l 37618 cdleme21ct 37625 cdleme21d 37626 cdleme21e 37627 cdleme26e 37655 cdleme26eALTN 37657 cdleme26fALTN 37658 cdleme26f 37659 cdleme26f2ALTN 37660 cdleme26f2 37661 cdleme39n 37762 cdlemh2 38112 cdlemh 38113 cdlemk12 38146 cdlemk12u 38168 cdlemkfid1N 38217 congsub 39911 mzpcong 39913 jm2.18 39929 jm2.15nn0 39944 jm2.27c 39948 |
Copyright terms: Public domain | W3C validator |