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

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

Proof of Theorem syl221anc
StepHypRef Expression
1 syl3anc.1 . 2 (𝜑𝜓)
2 syl3anc.2 . 2 (𝜑𝜒)
3 syl3anc.3 . . 3 (𝜑𝜃)
4 syl3Xanc.4 . . 3 (𝜑𝜏)
53, 4jca 513 . 2 (𝜑 → (𝜃𝜏))
6 syl23anc.5 . 2 (𝜑𝜂)
7 syl221anc.6 . 2 (((𝜓𝜒) ∧ (𝜃𝜏) ∧ 𝜂) → 𝜁)
81, 2, 5, 6, 7syl211anc 1377 1 (𝜑𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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 398  df-3an 1090
This theorem is referenced by:  syl222anc  1387  vtocldf  3511  f1oprswap  6829  dmdcand  11961  modmul12d  13831  modnegd  13832  modadd12d  13833  exprec  14010  rpexpmord  14074  splval2  14646  dvdsmodexp  16145  eulerthlem2  16655  fermltl  16657  odzdvds  16668  fnpr2o  17440  efgredleme  19526  efgredlemc  19528  blssps  23780  blss  23781  metequiv2  23869  met1stc  23880  met2ndci  23881  metdstri  24217  xlebnum  24331  caubl  24675  divcxp  26045  cxple2a  26057  cxplead  26079  cxplt2d  26084  cxple2d  26085  mulcxpd  26086  ang180  26167  wilthlem2  26421  lgsvalmod  26667  lgsmod  26674  lgsdir2lem4  26679  lgsdirprm  26682  lgsne0  26686  lgseisen  26730  conway  27141  ax5seglem9  27889  fzm1ne1  31695  xrsmulgzz  31872  linds2eq  32171  heiborlem8  36280  cdlemd4  38667  cdleme15a  38740  cdleme17b  38753  cdleme25a  38819  cdleme25c  38821  cdleme25dN  38822  cdleme26ee  38826  tendococl  39238  tendodi1  39250  tendodi2  39251  cdlemi  39286  tendocan  39290  cdlemk5a  39301  cdlemk5  39302  cdlemk10  39309  cdlemk5u  39327  cdlemkfid1N  39387  pellexlem6  41160  acongeq  41310  jm2.25  41326  stoweidlem42  44290  stoweidlem51  44299  ldepspr  46561
  Copyright terms: Public domain W3C validator