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 512 | . 2 ⊢ (𝜑 → (𝜁 ∧ 𝜎)) |
9 | syl322anc.8 | . 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎)) → 𝜌) | |
10 | 1, 2, 3, 4, 5, 8, 9 | syl321anc 1384 | 1 ⊢ (𝜑 → 𝜌) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1079 |
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 208 df-an 397 df-3an 1081 |
This theorem is referenced by: ax5seglem6 26647 ax5seg 26651 elpaddatriN 36819 paddasslem8 36843 paddasslem12 36847 paddasslem13 36848 pmodlem1 36862 osumcllem5N 36976 pexmidlem2N 36987 cdleme3h 37251 cdleme7ga 37264 cdleme20l 37338 cdleme21ct 37345 cdleme21d 37346 cdleme21e 37347 cdleme26e 37375 cdleme26eALTN 37377 cdleme26fALTN 37378 cdleme26f 37379 cdleme26f2ALTN 37380 cdleme26f2 37381 cdleme39n 37482 cdlemh2 37832 cdlemh 37833 cdlemk12 37866 cdlemk12u 37888 cdlemkfid1N 37937 congsub 39445 mzpcong 39447 jm2.18 39463 jm2.15nn0 39478 jm2.27c 39482 |
Copyright terms: Public domain | W3C validator |