![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > syl221anc | 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 | ⊢ (𝜑 → 𝜂) |
syl221anc.6 | ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁) |
Ref | Expression |
---|---|
syl221anc | ⊢ (𝜑 → 𝜁) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl3anc.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | syl3anc.2 | . 2 ⊢ (𝜑 → 𝜒) | |
3 | syl3anc.3 | . . 3 ⊢ (𝜑 → 𝜃) | |
4 | syl3Xanc.4 | . . 3 ⊢ (𝜑 → 𝜏) | |
5 | 3, 4 | jca 510 | . 2 ⊢ (𝜑 → (𝜃 ∧ 𝜏)) |
6 | syl23anc.5 | . 2 ⊢ (𝜑 → 𝜂) | |
7 | syl221anc.6 | . 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁) | |
8 | 1, 2, 5, 6, 7 | syl211anc 1373 | 1 ⊢ (𝜑 → 𝜁) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∧ w3a 1084 |
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 395 df-3an 1086 |
This theorem is referenced by: syl222anc 1383 vtocldf 3540 f1oprswap 6877 dmdcand 12062 modmul12d 13937 modnegd 13938 modadd12d 13939 exprec 14115 rpexpmord 14179 splval2 14758 dvdsmodexp 16257 eulerthlem2 16777 fermltl 16779 odzdvds 16790 fnpr2o 17565 efgredleme 19735 efgredlemc 19737 blssps 24416 blss 24417 metequiv2 24505 met1stc 24516 met2ndci 24517 metdstri 24853 xlebnum 24977 caubl 25322 divcxp 26709 cxple2a 26721 cxplead 26743 cxplt2d 26748 cxple2d 26749 mulcxpd 26750 ang180 26837 wilthlem2 27092 lgsvalmod 27340 lgsmod 27347 lgsdir2lem4 27352 lgsdirprm 27355 lgsne0 27359 lgseisen 27403 conway 27824 ax5seglem9 28866 fzm1ne1 32692 xrsmulgzz 32890 linds2eq 33260 heiborlem8 37530 cdlemd4 39911 cdleme15a 39984 cdleme17b 39997 cdleme25a 40063 cdleme25c 40065 cdleme25dN 40066 cdleme26ee 40070 tendococl 40482 tendodi1 40494 tendodi2 40495 cdlemi 40530 tendocan 40534 cdlemk5a 40545 cdlemk5 40546 cdlemk10 40553 cdlemk5u 40571 cdlemkfid1N 40631 pellexlem6 42526 acongeq 42676 jm2.25 42692 stoweidlem42 45697 stoweidlem51 45706 ldepspr 47890 |
Copyright terms: Public domain | W3C validator |