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

Theorem syl221anc 1379
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 511 . 2 (𝜑 → (𝜃𝜏))
6 syl23anc.5 . 2 (𝜑𝜂)
7 syl221anc.6 . 2 (((𝜓𝜒) ∧ (𝜃𝜏) ∧ 𝜂) → 𝜁)
81, 2, 5, 6, 7syl211anc 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