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 511 | . 2 ⊢ (𝜑 → (𝜃 ∧ 𝜏)) |
6 | syl23anc.5 | . 2 ⊢ (𝜑 → 𝜂) | |
7 | syl221anc.6 | . 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁) | |
8 | 1, 2, 5, 6, 7 | syl211anc 1374 | 1 ⊢ (𝜑 → 𝜁) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1085 |
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 1087 |
This theorem is referenced by: syl222anc 1384 vtocldf 3483 f1oprswap 6743 dmdcand 11710 modmul12d 13573 modnegd 13574 modadd12d 13575 exprec 13752 rpexpmord 13814 splval2 14398 dvdsmodexp 15899 eulerthlem2 16411 fermltl 16413 odzdvds 16424 fnpr2o 17185 efgredleme 19264 efgredlemc 19266 blssps 23485 blss 23486 metequiv2 23572 met1stc 23583 met2ndci 23584 metdstri 23920 xlebnum 24034 caubl 24377 divcxp 25747 cxple2a 25759 cxplead 25781 cxplt2d 25786 cxple2d 25787 mulcxpd 25788 ang180 25869 wilthlem2 26123 lgsvalmod 26369 lgsmod 26376 lgsdir2lem4 26381 lgsdirprm 26384 lgsne0 26388 lgseisen 26432 ax5seglem9 27208 fzm1ne1 31012 xrsmulgzz 31189 linds2eq 31477 conway 33920 heiborlem8 35903 cdlemd4 38142 cdleme15a 38215 cdleme17b 38228 cdleme25a 38294 cdleme25c 38296 cdleme25dN 38297 cdleme26ee 38301 tendococl 38713 tendodi1 38725 tendodi2 38726 cdlemi 38761 tendocan 38765 cdlemk5a 38776 cdlemk5 38777 cdlemk10 38784 cdlemk5u 38802 cdlemkfid1N 38862 pellexlem6 40572 acongeq 40721 jm2.25 40737 stoweidlem42 43473 stoweidlem51 43482 ldepspr 45702 |
Copyright terms: Public domain | W3C validator |