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  2043  2reu5  3193  f1ocnvfvrneq  5964  fcof1o  5971  isoselem  6006  isose  6008  fnwelem  6644  tposss  6663  smoiso  6736  nneob  7007  difsnen  7302  ordtypelem10  7608  oismo  7621  cantnfcl  7734  cantnflt2  7740  oemapso  7750  cantnf  7761  mapfien  7765  scott0  7924  tskwe  7951  infxpenlem  8009  ac10ct  8029  acndom  8046  dfac12lem2  8138  dfac12r  8140  pwcdadom  8210  ackbij1lem15  8228  ackbij2lem2  8234  ackbij2lem3  8235  ackbij2  8237  fin23lem22  8321  domtriomlem  8436  axdc3lem2  8445  sdomsdomcard  8549  canthp1lem2  8642  pwfseqlem5  8652  gchhar  8668  fzssp1  11300  fzosplitsnm1  11403  fzofzp1  11416  fzostep1  11427  bcm1k  11883  swrdccat2  12139  revccat  12192  revrev  12193  climuni  12816  isercolllem2  12929  isercoll  12931  serf0  12944  fsumparts  13055  hashiun  13071  isumsup2  13095  climcndslem1  13098  climcndslem2  13099  oddprm  13668  vdwmc  13825  prdsplusg  14172  prdsvsca  14174  imasdsval2  14233  sscpwex  14506  ssc2  14513  odcl2  15704  lsmmod  15810  efgsdmi  15867  gsumval3  16017  gsumzinv  16043  ablfac1b  16131  pgpfac1lem1  16135  pgpfaclem2  16143  ablfaclem2  16147  ablfac  16149  srng0  16451  znzrh2  17329  znf1o  17335  znhash  17342  znfld  17344  cygznlem3  17353  ip2di  17375  iscncl  17836  qtopcmap  18255  hmeores  18307  qtopf1  18352  fbssfi  18373  filssufil  18448  fmfnfmlem3  18492  clssubg  18642  tmsxms  19020  prdsxms  19064  metustfbas  19100  metuel2  19113  restmetu  19121  nrginvrcn  19231  nmhmcn  19632  iscmet3  19750  minveclem3  19834  ovoliunlem2  19903  ismbf3d  20048  i1fd  20075  dvadd  20330  dvmul  20331  dvaddf  20332  dvco  20337  dvcof  20338  dvcnvlem  20364  mpfsubrg  20465  pf1subrg  20472  mpfpf1  20475  pf1mpf  20476  mdeglt  20492  dgrub  20657  plyremlem  20725  fta1lem  20728  fta1  20729  vieta1lem2  20732  plyexmo  20734  elaa  20737  ulmcau  20815  ulmdvlem3  20822  ppinprm  21444  chtnprm  21446  dchrzrh1  21537  dchr1  21550  dchr1re  21556  dchrptlem1  21557  dchrpt  21560  dchrsum2  21561  dchrhash  21564  rpvmasumlem  21690  rpvmasum2  21715  mudivsum  21733  cyclnspth  22127  usgravd0nedg  22192  subgores  22401  rngosn  22501  minvecolem3  22887  orngmullt  24929  pl1cn  25055  zrhunitpreima  25078  qqhnm  25090  qqhucn  25092  ddemeas  25323  1stmbfm  25346  2ndmbfm  25347  unveldomd  25439  probmeasb  25454  signstfvp  25614  signstres  25618  subfacp1lem5  25709  erdsze2lem1  25728  cvmseu  25802  cvmliftlem11  25821  cvmlift3lem8  25852  cvmlift3lem9  25853  ghomfo  25941  relexpsucr  25963  binomfallfaclem2  26186  wfrlem5  26372  frrlem5  26416  meran1  26991  lukshef-ax2  26995  ordcmp  27027  mblfinlem2  27100  trer  27182  sdclem2  27309  ismtyhmeolem  27376  heiborlem10  27392  aomclem6  28063  kelac1  28067  kelac2  28069  isnumbasgrplem3  28176  pmtrfv  28301  symgtrinv  28319  proot1mul  28421  stoweidlem11  28660  stoweidlem14  28663  afv0nbfvbi  28913  el2spthonot  29248  bnj1098  30347  axc11nlem5NEW11  30747  lpssat  31084  lssatle  31086  lssat  31087  cdlemk45  33017  dia2dimlem9  33143  diblsmopel  33242  dochspss  33449  baerlem5blem2  33783  hdmap14lem4a  33945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator