MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl221anc Structured version   Visualization version   GIF version

Theorem syl221anc 1488
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
syl12anc.1 (𝜑𝜓)
syl12anc.2 (𝜑𝜒)
syl12anc.3 (𝜑𝜃)
syl22anc.4 (𝜑𝜏)
syl23anc.5 (𝜑𝜂)
syl221anc.6 (((𝜓𝜒) ∧ (𝜃𝜏) ∧ 𝜂) → 𝜁)
Assertion
Ref Expression
syl221anc (𝜑𝜁)

Proof of Theorem syl221anc
StepHypRef Expression
1 syl12anc.1 . 2 (𝜑𝜓)
2 syl12anc.2 . 2 (𝜑𝜒)
3 syl12anc.3 . . 3 (𝜑𝜃)
4 syl22anc.4 . . 3 (𝜑𝜏)
53, 4jca 555 . 2 (𝜑 → (𝜃𝜏))
6 syl23anc.5 . 2 (𝜑𝜂)
7 syl221anc.6 . 2 (((𝜓𝜒) ∧ (𝜃𝜏) ∧ 𝜂) → 𝜁)
81, 2, 5, 6, 7syl211anc 1483 1 (𝜑𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
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 197  df-an 385  df-3an 1074
This theorem is referenced by:  syl222anc  1493  vtocldf  3396  f1oprswap  6342  dmdcand  11042  modmul12d  12938  modnegd  12939  modadd12d  12940  exprec  13115  splval2  13728  dvdsmodexp  15210  eulerthlem2  15709  fermltl  15711  odzdvds  15722  efgredleme  18376  efgredlemc  18378  blssps  22450  blss  22451  metequiv2  22536  met1stc  22547  met2ndci  22548  metdstri  22875  xlebnum  22985  caubl  23326  divcxp  24653  cxple2a  24665  cxplead  24687  cxplt2d  24692  cxple2d  24693  mulcxpd  24694  ang180  24764  wilthlem2  25015  lgsvalmod  25261  lgsmod  25268  lgsdir2lem4  25273  lgsdirprm  25276  lgsne0  25280  lgseisen  25324  ax5seglem9  26037  xrsmulgzz  30008  conway  32237  etasslt  32247  heiborlem8  33948  cdlemd4  36009  cdleme15a  36082  cdleme17b  36095  cdleme25a  36161  cdleme25c  36163  cdleme25dN  36164  cdleme26ee  36168  tendococl  36580  tendodi1  36592  tendodi2  36593  cdlemi  36628  tendocan  36632  cdlemk5a  36643  cdlemk5  36644  cdlemk10  36651  cdlemk5u  36669  cdlemkfid1N  36729  pellexlem6  37918  rpexpmord  38033  acongeq  38070  jm2.25  38086  stoweidlem42  40780  stoweidlem51  40789  ldepspr  42790
  Copyright terms: Public domain W3C validator