![]() |
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 507 | . 2 ⊢ (𝜑 → (𝜂 ∧ 𝜁)) |
8 | syl222anc.7 | . 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁)) → 𝜎) | |
9 | 1, 2, 3, 4, 7, 8 | syl221anc 1449 | 1 ⊢ (𝜑 → 𝜎) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∧ w3a 1071 |
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 199 df-an 387 df-3an 1073 |
This theorem is referenced by: 3anandis 1544 3anandirs 1545 omopth2 7948 omeu 7949 dfac12lem2 9301 xaddass2 12392 xpncan 12393 divdenle 15861 pockthlem 16013 znidomb 20305 tanord1 24721 ang180lem5 24991 isosctrlem3 24998 log2tlbnd 25124 basellem1 25259 perfectlem2 25407 bposlem6 25466 dchrisum0flblem2 25650 pntpbnd1a 25726 axcontlem8 26320 xlt2addrd 30088 xrge0addass 30252 xrge0npcan 30256 submatminr1 30474 carsgclctunlem2 30979 4atexlemntlpq 36206 4atexlemnclw 36208 trlval2 36301 cdleme0moN 36363 cdleme16b 36417 cdleme16c 36418 cdleme16d 36419 cdleme16e 36420 cdleme17c 36426 cdlemeda 36436 cdleme20h 36454 cdleme20j 36456 cdleme20l2 36459 cdleme21c 36465 cdleme21ct 36467 cdleme22aa 36477 cdleme22cN 36480 cdleme22d 36481 cdleme22e 36482 cdleme22eALTN 36483 cdleme23b 36488 cdleme25a 36491 cdleme25dN 36494 cdleme27N 36507 cdleme28a 36508 cdleme28b 36509 cdleme29ex 36512 cdleme32c 36581 cdleme42k 36622 cdlemg2cex 36729 cdlemg2idN 36734 cdlemg31c 36837 cdlemk5a 36973 cdlemk5 36974 congmul 38475 jm2.25lem1 38506 jm2.26 38510 jm2.27a 38513 infleinflem1 40476 stoweidlem42 41168 |
Copyright terms: Public domain | W3C validator |