![]() |
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 |
---|---|
syl3anc.1 | ⊢ (𝜑 → 𝜓) |
syl3anc.2 | ⊢ (𝜑 → 𝜒) |
syl3anc.3 | ⊢ (𝜑 → 𝜃) |
syl3Xanc.4 | ⊢ (𝜑 → 𝜏) |
syl23anc.5 | ⊢ (𝜑 → 𝜂) |
syl33anc.6 | ⊢ (𝜑 → 𝜁) |
syl222anc.7 | ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁)) → 𝜎) |
Ref | Expression |
---|---|
syl222anc | ⊢ (𝜑 → 𝜎) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl3anc.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | syl3anc.2 | . 2 ⊢ (𝜑 → 𝜒) | |
3 | syl3anc.3 | . 2 ⊢ (𝜑 → 𝜃) | |
4 | syl3Xanc.4 | . 2 ⊢ (𝜑 → 𝜏) | |
5 | syl23anc.5 | . . 3 ⊢ (𝜑 → 𝜂) | |
6 | syl33anc.6 | . . 3 ⊢ (𝜑 → 𝜁) | |
7 | 5, 6 | jca 511 | . 2 ⊢ (𝜑 → (𝜂 ∧ 𝜁)) |
8 | syl222anc.7 | . 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁)) → 𝜎) | |
9 | 1, 2, 3, 4, 7, 8 | syl221anc 1380 | 1 ⊢ (𝜑 → 𝜎) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 |
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 206 df-an 396 df-3an 1088 |
This theorem is referenced by: 3anandis 1470 3anandirs 1471 omopth2 8590 omeu 8591 dfac12lem2 10145 xaddass2 13236 xpncan 13237 divdenle 16692 pockthlem 16845 znidomb 21340 tanord1 26297 ang180lem5 26569 isosctrlem3 26576 log2tlbnd 26701 basellem1 26836 perfectlem2 26984 bposlem6 27043 dchrisum0flblem2 27263 pntpbnd1a 27339 mulsproplem1 27826 axcontlem8 28511 xlt2addrd 32253 s2f1 32393 xrge0addass 32473 xrge0npcan 32477 submatminr1 33103 carsgclctunlem2 33631 4atexlemntlpq 39255 4atexlemnclw 39257 trlval2 39350 cdleme0moN 39412 cdleme16b 39466 cdleme16c 39467 cdleme16d 39468 cdleme16e 39469 cdleme17c 39475 cdlemeda 39485 cdleme20h 39503 cdleme20j 39505 cdleme20l2 39508 cdleme21c 39514 cdleme21ct 39516 cdleme22aa 39526 cdleme22cN 39529 cdleme22d 39530 cdleme22e 39531 cdleme22eALTN 39532 cdleme23b 39537 cdleme25a 39540 cdleme25dN 39543 cdleme27N 39556 cdleme28a 39557 cdleme28b 39558 cdleme29ex 39561 cdleme32c 39630 cdleme42k 39671 cdlemg2cex 39778 cdlemg2idN 39783 cdlemg31c 39886 cdlemk5a 40022 cdlemk5 40023 congmul 42021 jm2.25lem1 42052 jm2.26 42056 jm2.27a 42059 infleinflem1 44391 stoweidlem42 45069 |
Copyright terms: Public domain | W3C validator |