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 554 | . 2 ⊢ (𝜑 → (𝜁 ∧ 𝜎)) |
9 | syl322anc.8 | . 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎)) → 𝜌) | |
10 | 1, 2, 3, 4, 5, 8, 9 | syl321anc 1348 | 1 ⊢ (𝜑 → 𝜌) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 384 ∧ w3a 1037 |
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 197 df-an 386 df-3an 1039 |
This theorem is referenced by: ax5seglem6 25814 ax5seg 25818 elpaddatriN 35089 paddasslem8 35113 paddasslem12 35117 paddasslem13 35118 pmodlem1 35132 osumcllem5N 35246 pexmidlem2N 35257 cdleme3h 35522 cdleme7ga 35535 cdleme20l 35610 cdleme21ct 35617 cdleme21d 35618 cdleme21e 35619 cdleme26e 35647 cdleme26eALTN 35649 cdleme26fALTN 35650 cdleme26f 35651 cdleme26f2ALTN 35652 cdleme26f2 35653 cdleme39n 35754 cdlemh2 36104 cdlemh 36105 cdlemk12 36138 cdlemk12u 36160 cdlemkfid1N 36209 congsub 37537 mzpcong 37539 jm2.18 37555 jm2.15nn0 37570 jm2.27c 37574 |
Copyright terms: Public domain | W3C validator |