MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  4syl Unicode version

Theorem 4syl 20
Description: Inference chaining three syllogisms. The use of this theorem is marked "discouraged" because it can cause the "minimize" command to have very long run times. However, feel free to use "minimize 4syl /override" if you wish. Remember to update the Travis "discouraged" file if it gets used. (Contributed by BJ, 14-Jul-2018.) (New usage is discouraged.)
Hypotheses
Ref Expression
4syl.1
4syl.2
4syl.3
4syl.4
Assertion
Ref Expression
4syl

Proof of Theorem 4syl
StepHypRef Expression
1 4syl.1 . . 3
2 4syl.2 . . 3
3 4syl.3 . . 3
41, 2, 33syl 19 . 2
5 4syl.4 . 2
64, 5syl 16 1
Colors of variables: wff set class
Syntax hints:  ->wi 4
This theorem is referenced by:  aevlem1  2051  2reu5  3205  f1ocnvfvrneq  6000  fcof1o  6007  isoselem  6042  isose  6044  fnwelem  6693  tposss  6712  smoiso  6786  nneob  7057  difsnen  7355  ordtypelem10  7663  oismo  7676  cantnfcl  7789  cantnflt2  7795  oemapso  7805  cantnf  7816  mapfien  7820  scott0  7979  tskwe  8006  infxpenlem  8066  ac10ct  8086  acndom  8103  dfac12lem2  8195  dfac12r  8197  pwcdadom  8267  ackbij1lem15  8285  ackbij2lem2  8291  ackbij2lem3  8292  ackbij2  8294  fin23lem22  8378  domtriomlem  8493  axdc3lem2  8502  sdomsdomcard  8606  canthp1lem2  8699  pwfseqlem5  8709  gchhar  8725  fzssp1  11357  fzosplitsnm1  11460  fzofzp1  11473  fzostep1  11484  bcm1k  11940  swrdccat2  12199  revccat  12253  revrev  12254  climuni  12877  isercolllem2  12990  isercoll  12992  serf0  13005  fsumparts  13116  hashiun  13132  isumsup2  13156  climcndslem1  13159  climcndslem2  13160  oddprm  13729  vdwmc  13886  prdsplusg  14235  prdsvsca  14237  imasdsval2  14296  sscpwex  14569  ssc2  14576  odcl2  15810  lsmmod  15916  efgsdmi  15973  gsumval3  16124  gsumzinv  16150  ablfac1b  16243  pgpfac1lem1  16247  pgpfaclem2  16255  ablfaclem2  16259  ablfac  16261  srng0  16564  znzrh2  17451  znf1o  17457  znhash  17464  znfld  17466  cygznlem3  17475  ip2di  17497  pmtrfv  17609  symgtrinv  17628  iscncl  18347  qtopcmap  18766  hmeores  18818  qtopf1  18863  fbssfi  18884  filssufil  18959  fmfnfmlem3  19003  clssubg  19153  tmsxms  19531  prdsxms  19575  metustfbas  19611  metuel2  19624  restmetu  19632  nrginvrcn  19742  nmhmcn  20143  iscmet3  20261  minveclem3  20345  ovoliunlem2  20414  ismbf3d  20559  i1fd  20586  dvadd  20841  dvmul  20842  dvaddf  20843  dvco  20848  dvcof  20849  dvcnvlem  20875  mpfsubrg  20976  pf1subrg  20983  mpfpf1  20986  pf1mpf  20987  mdeglt  21003  dgrub  21168  plyremlem  21236  fta1lem  21239  fta1  21240  vieta1lem2  21243  plyexmo  21245  elaa  21248  ulmcau  21326  ulmdvlem3  21333  ppinprm  21956  chtnprm  21958  dchrzrh1  22049  dchr1  22062  dchr1re  22068  dchrptlem1  22069  dchrpt  22072  dchrsum2  22073  dchrhash  22076  rpvmasumlem  22202  rpvmasum2  22227  mudivsum  22245  cyclnspth  22639  usgravd0nedg  22704  subgores  22913  rngosn  23013  minvecolem3  23399  orngmullt  25438  pl1cn  25564  zrhunitpreima  25587  qqhnm  25599  qqhucn  25601  ddemeas  25832  1stmbfm  25855  2ndmbfm  25856  unveldomd  25948  probmeasb  25963  signstfvp  26123  signstres  26127  subfacp1lem5  26218  erdsze2lem1  26237  cvmseu  26311  cvmliftlem11  26330  cvmlift3lem8  26361  cvmlift3lem9  26362  ghomfo  26450  relexpsucr  26472  binomfallfaclem2  26695  wfrlem5  26881  frrlem5  26925  meran1  27500  lukshef-ax2  27504  ordcmp  27536  mblfinlem2  27609  trer  27691  sdclem2  27818  ismtyhmeolem  27885  heiborlem10  27901  aomclem6  28560  kelac1  28564  kelac2  28566  isnumbasgrplem3  28610  proot1mul  28746  stoweidlem11  28985  stoweidlem14  28988  afv0nbfvbi  29236  el2spthonot  29570  bnj1098  30624  axc11nlem5NEW11  31024  lpssat  31361  lssatle  31363  lssat  31364  cdlemk45  33294  dia2dimlem9  33420  diblsmopel  33519  dochspss  33726  baerlem5blem2  34060  hdmap14lem4a  34222
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator