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 515 | . 2 ⊢ (𝜑 → (𝜃 ∧ 𝜏)) |
6 | syl23anc.5 | . 2 ⊢ (𝜑 → 𝜂) | |
7 | syl221anc.6 | . 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁) | |
8 | 1, 2, 5, 6, 7 | syl211anc 1378 | 1 ⊢ (𝜑 → 𝜁) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1089 |
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 210 df-an 400 df-3an 1091 |
This theorem is referenced by: syl222anc 1388 vtocldf 3462 f1oprswap 6693 dmdcand 11620 modmul12d 13481 modnegd 13482 modadd12d 13483 exprec 13659 rpexpmord 13721 splval2 14305 dvdsmodexp 15804 eulerthlem2 16316 fermltl 16318 odzdvds 16329 fnpr2o 17034 efgredleme 19105 efgredlemc 19107 blssps 23294 blss 23295 metequiv2 23380 met1stc 23391 met2ndci 23392 metdstri 23720 xlebnum 23834 caubl 24177 divcxp 25547 cxple2a 25559 cxplead 25581 cxplt2d 25586 cxple2d 25587 mulcxpd 25588 ang180 25669 wilthlem2 25923 lgsvalmod 26169 lgsmod 26176 lgsdir2lem4 26181 lgsdirprm 26184 lgsne0 26188 lgseisen 26232 ax5seglem9 27000 fzm1ne1 30802 xrsmulgzz 30978 linds2eq 31261 conway 33687 heiborlem8 35670 cdlemd4 37909 cdleme15a 37982 cdleme17b 37995 cdleme25a 38061 cdleme25c 38063 cdleme25dN 38064 cdleme26ee 38068 tendococl 38480 tendodi1 38492 tendodi2 38493 cdlemi 38528 tendocan 38532 cdlemk5a 38543 cdlemk5 38544 cdlemk10 38551 cdlemk5u 38569 cdlemkfid1N 38629 pellexlem6 40311 acongeq 40460 jm2.25 40476 stoweidlem42 43212 stoweidlem51 43221 ldepspr 45441 |
Copyright terms: Public domain | W3C validator |