![]() |
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 555 | . 2 ⊢ (𝜑 → (𝜂 ∧ 𝜁)) |
8 | syl222anc.7 | . 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁)) → 𝜎) | |
9 | 1, 2, 3, 4, 7, 8 | syl221anc 1488 | 1 ⊢ (𝜑 → 𝜎) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1072 |
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 385 df-3an 1074 |
This theorem is referenced by: 3anandis 1583 3anandirs 1584 omopth2 7835 omeu 7836 dfac12lem2 9178 xaddass2 12293 xpncan 12294 divdenle 15679 pockthlem 15831 znidomb 20132 tanord1 24503 ang180lem5 24763 isosctrlem3 24770 log2tlbnd 24892 basellem1 25027 perfectlem2 25175 bposlem6 25234 dchrisum0flblem2 25418 pntpbnd1a 25494 axcontlem8 26071 xlt2addrd 29853 xrge0addass 30020 xrge0npcan 30024 submatminr1 30206 carsgclctunlem2 30711 4atexlemntlpq 35875 4atexlemnclw 35877 trlval2 35971 cdleme0moN 36033 cdleme16b 36087 cdleme16c 36088 cdleme16d 36089 cdleme16e 36090 cdleme17c 36096 cdlemeda 36106 cdleme20h 36124 cdleme20j 36126 cdleme20l2 36129 cdleme21c 36135 cdleme21ct 36137 cdleme22aa 36147 cdleme22cN 36150 cdleme22d 36151 cdleme22e 36152 cdleme22eALTN 36153 cdleme23b 36158 cdleme25a 36161 cdleme25dN 36164 cdleme27N 36177 cdleme28a 36178 cdleme28b 36179 cdleme29ex 36182 cdleme32c 36251 cdleme42k 36292 cdlemg2cex 36399 cdlemg2idN 36404 cdlemg31c 36507 cdlemk5a 36643 cdlemk5 36644 congmul 38054 jm2.25lem1 38085 jm2.26 38089 jm2.27a 38092 infleinflem1 40102 stoweidlem42 40780 |
Copyright terms: Public domain | W3C validator |