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

Theorem 4syl 21
Description: Inference chaining three syllogisms syl 16. (Contributed by BJ, 14-Jul-2018.) 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. (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 20 . 2
5 4syl.4 . 2
64, 5syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4
This theorem is referenced by:  aevlem1  1939  aevlem1OLD  2060  eqeq1d  2459  2reu5  3308  f1ocnvfvrneq  6189  isoselem  6237  isose  6239  fnwelem  6915  tposss  6975  smoiso  7052  nneob  7320  difsnen  7619  ordtypelem10  7973  oismo  7986  cantnflt2  8113  oemapso  8122  cantnf  8133  cantnfclOLD  8137  cantnflt2OLD  8143  cantnfOLD  8155  mapfienOLD  8159  scott0  8325  tskwe  8352  infxpenlem  8412  ac10ct  8436  acndom  8453  dfac12lem2  8545  dfac12r  8547  pwcdadom  8617  ackbij1lem15  8635  ackbij2lem2  8641  ackbij2lem3  8642  ackbij2  8644  fin23lem22  8728  domtriomlem  8843  axdc3lem2  8852  sdomsdomcard  8956  canthp1lem2  9052  pwfseqlem5  9062  gchhar  9078  fzssp1  11755  fzosplitsnm1  11890  fzofzp1  11909  fzostep1  11922  bcm1k  12393  swrdccat2  12683  revccat  12740  revrev  12741  climuni  13375  isercolllem2  13488  isercoll  13490  serf0  13503  fsumparts  13620  hashiun  13636  isumsup2  13658  climcndslem1  13661  climcndslem2  13662  oddprm  14339  vdwmc  14496  prdsplusg  14855  prdsvsca  14857  imasdsval2  14913  sscpwex  15184  ssc2  15191  pmtrfv  16477  symgtrinv  16497  odcl2  16587  lsmmod  16693  efgsdmi  16750  gsumval3OLD  16908  gsumzinv  16969  gsumzinvOLD  16970  ablfac1b  17121  pgpfac1lem1  17125  pgpfaclem2  17133  ablfaclem2  17137  ablfac  17139  srng0  17509  mpfsubrg  18201  pf1subrg  18384  mpfpf1  18387  pf1mpf  18388  znzrh2  18584  znf1o  18590  znhash  18597  znfld  18599  cygznlem3  18608  ip2di  18676  iscncl  19770  qtopcmap  20220  hmeores  20272  qtopf1  20317  fbssfi  20338  filssufil  20413  fmfnfmlem3  20457  clssubg  20607  tmsxms  20989  prdsxms  21033  metustfbas  21069  metuel2  21082  restmetu  21090  nrginvrcn  21200  nmhmcn  21603  iscmet3  21732  minveclem3  21844  ovoliunlem2  21914  ismbf3d  22061  i1fd  22088  dvadd  22343  dvmul  22344  dvaddf  22345  dvco  22350  dvcof  22351  dvcnvlem  22377  mdeglt  22465  dgrub  22631  plyremlem  22700  fta1lem  22703  fta1  22704  vieta1lem2  22707  plyexmo  22709  elaa  22712  ulmcau  22790  ulmdvlem3  22797  ppinprm  23426  chtnprm  23428  dchrzrh1  23519  dchr1  23532  dchr1re  23538  dchrptlem1  23539  dchrpt  23542  dchrsum2  23543  dchrhash  23546  rpvmasumlem  23672  rpvmasum2  23697  mudivsum  23715  f1otrg  24174  cyclnspth  24631  el2spthonot  24870  usgravd0nedg  24918  subgores  25306  rngosn  25406  minvecolem3  25792  orngmullt  27799  locfinref  27844  pl1cn  27937  zrhunitpreima  27959  qqhnm  27971  qqhucn  27973  ddemeas  28208  1stmbfm  28231  2ndmbfm  28232  omsval  28264  unveldomd  28354  probmeasb  28369  signstfvp  28528  signstres  28532  subfacp1lem5  28628  erdsze2lem1  28647  cvmseu  28721  cvmliftlem11  28740  cvmlift3lem8  28771  cvmlift3lem9  28772  ghomfo  29031  relexpsucr  29053  binomfallfaclem2  29162  wfrlem5  29347  frrlem5  29391  meran1  29876  lukshef-ax2  29880  ordcmp  29912  wl-nfeqfb  29990  mblfinlem2  30052  trer  30134  sdclem2  30235  ismtyhmeolem  30300  heiborlem10  30316  aomclem6  31005  kelac1  31009  kelac2  31011  isnumbasgrplem3  31054  proot1mul  31156  stoweidlem11  31793  stoweidlem14  31796  afv0nbfvbi  32236  bnj1098  33842  bj-aevlem1v  34320  lpssat  34738  lssatle  34740  lssat  34741  cdlemk45  36673  dia2dimlem9  36799  diblsmopel  36898  dochspss  37105  baerlem5blem2  37439  hdmap14lem4a  37601
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator