Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > syl222anc | 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 | ⊢ (𝜑 → 𝜁) |
syl222anc.7 | ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁)) → 𝜎) |
Ref | Expression |
---|---|
syl222anc | ⊢ (𝜑 → 𝜎) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl12anc.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | syl12anc.2 | . 2 ⊢ (𝜑 → 𝜒) | |
3 | syl12anc.3 | . 2 ⊢ (𝜑 → 𝜃) | |
4 | syl22anc.4 | . 2 ⊢ (𝜑 → 𝜏) | |
5 | syl23anc.5 | . . 3 ⊢ (𝜑 → 𝜂) | |
6 | syl33anc.6 | . . 3 ⊢ (𝜑 → 𝜁) | |
7 | 5, 6 | jca 553 | . 2 ⊢ (𝜑 → (𝜂 ∧ 𝜁)) |
8 | syl222anc.7 | . 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁)) → 𝜎) | |
9 | 1, 2, 3, 4, 7, 8 | syl221anc 1329 | 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: 3anandis 1426 3anandirs 1427 omopth2 7551 omeu 7552 dfac12lem2 8849 xaddass2 11952 xpncan 11953 divdenle 15295 pockthlem 15447 znidomb 19729 tanord1 24087 ang180lem5 24343 isosctrlem3 24350 log2tlbnd 24472 basellem1 24607 perfectlem2 24755 bposlem6 24814 dchrisum0flblem2 24998 pntpbnd1a 25074 axcontlem8 25651 xlt2addrd 28913 xrge0addass 29021 xrge0npcan 29025 submatminr1 29204 carsgclctunlem2 29708 4atexlemntlpq 34372 4atexlemnclw 34374 trlval2 34468 cdleme0moN 34530 cdleme16b 34584 cdleme16c 34585 cdleme16d 34586 cdleme16e 34587 cdleme17c 34593 cdlemeda 34603 cdleme20h 34622 cdleme20j 34624 cdleme20l2 34627 cdleme21c 34633 cdleme21ct 34635 cdleme22aa 34645 cdleme22cN 34648 cdleme22d 34649 cdleme22e 34650 cdleme22eALTN 34651 cdleme23b 34656 cdleme25a 34659 cdleme25dN 34662 cdleme27N 34675 cdleme28a 34676 cdleme28b 34677 cdleme29ex 34680 cdleme32c 34749 cdleme42k 34790 cdlemg2cex 34897 cdlemg2idN 34902 cdlemg31c 35005 cdlemk5a 35141 cdlemk5 35142 congmul 36552 jm2.25lem1 36583 jm2.26 36587 jm2.27a 36590 infleinflem1 38527 stoweidlem42 38935 |
Copyright terms: Public domain | W3C validator |