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 causes the "minimize" command to have very long run times. However, feel free to override it to use directly or in small "minimize" runs. (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  2054  2reu5  3155  f1ocnvfvrneq  6071  fcof1o  6078  isoselem  6113  isose  6115  fnwelem  6515  tposss  6534  smoiso  6677  nneob  6948  difsnen  7243  ordtypelem10  7549  oismo  7562  cantnfcl  7675  cantnflt2  7681  oemapso  7691  cantnf  7702  mapfien  7706  scott0  7865  tskwe  7892  infxpenlem  7950  ac10ct  7970  acndom  7987  dfac12lem2  8079  dfac12r  8081  pwcdadom  8151  ackbij1lem15  8169  ackbij2lem2  8175  ackbij2lem3  8176  ackbij2  8178  fin23lem22  8262  domtriomlem  8377  axdc3lem2  8386  sdomsdomcard  8490  canthp1lem2  8583  pwfseqlem5  8593  gchhar  8609  fzssp1  11150  fzofzp1  11244  fzostep1  11252  bcm1k  11661  swrdccat2  11830  revccat  11853  revrev  11854  climuni  12401  isercolllem2  12514  isercoll  12516  serf0  12529  fsumparts  12640  hashiun  12656  isumsup2  12681  climcndslem1  12684  climcndslem2  12685  oddprm  13244  vdwmc  13401  prdsplusg  13736  prdsvsca  13738  imasdsval2  13797  sscpwex  14070  ssc2  14077  odcl2  15237  lsmmod  15343  efgsdmi  15400  gsumval3  15550  gsumzinv  15576  ablfac1b  15664  pgpfac1lem1  15668  pgpfaclem2  15676  ablfaclem2  15680  ablfac  15682  srng0  15984  znzrh2  16862  znf1o  16868  znhash  16875  znfld  16877  cygznlem3  16886  ip2di  16908  iscncl  17369  qtopcmap  17787  hmeores  17839  qtopf1  17884  fbssfi  17905  filssufil  17980  fmfnfmlem3  18024  clssubg  18174  tmsxms  18552  prdsxms  18596  metustfbas  18632  metuel2  18645  restmetu  18653  nrginvrcn  18763  nmhmcn  19164  iscmet3  19282  minveclem3  19366  ovoliunlem2  19435  ismbf3d  19580  i1fd  19607  dvadd  19862  dvmul  19863  dvaddf  19864  dvco  19869  dvcof  19870  dvcnvlem  19896  mpfsubrg  19997  pf1subrg  20004  mpfpf1  20007  pf1mpf  20008  mdeglt  20024  dgrub  20189  plyremlem  20257  fta1lem  20260  fta1  20261  vieta1lem2  20264  plyexmo  20266  elaa  20269  ulmcau  20347  ulmdvlem3  20354  ppinprm  20971  chtnprm  20973  dchrzrh1  21064  dchr1  21077  dchr1re  21083  dchrptlem1  21084  dchrpt  21087  dchrsum2  21088  dchrhash  21091  rpvmasumlem  21217  rpvmasum2  21242  mudivsum  21260  cyclnspth  21654  usgravd0nedg  21719  subgores  21928  rngosn  22028  minvecolem3  22414  zrhunitpreima  24576  qqhnm  24588  qqhucn  24590  1stmbfm  24840  2ndmbfm  24841  unveldomd  24933  probmeasb  24948  subfacp1lem5  25130  erdsze2lem1  25149  cvmseu  25223  cvmliftlem11  25242  cvmlift3lem8  25273  cvmlift3lem9  25274  ghomfo  25362  relexpsucr  25390  binomfallfaclem2  25616  wfrlem5  25802  frrlem5  25846  meran1  26421  lukshef-ax2  26425  ordcmp  26457  mblfinlem2  26509  trer  26586  sdclem2  26713  ismtyhmeolem  26780  heiborlem10  26796  aomclem6  27469  kelac1  27473  kelac2  27475  isnumbasgrplem3  27582  pmtrfv  27707  symgtrinv  27725  proot1mul  27827  stoweidlem11  28070  stoweidlem14  28073  afv0nbfvbi  28326  fzosplitsnm1  28474  el2spthonot  28722  bnj1098  29551  ax10lem5NEW7  29869  lpssat  30207  lssatle  30209  lssat  30210  cdlemk45  32140  dia2dimlem9  32266  diblsmopel  32365  dochspss  32572  baerlem5blem2  32906  hdmap14lem4a  33068
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator