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

Theorem 4syl 19
 Description: Inference chaining three syllogisms syl 17. (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 18 . 2 (𝜑𝜃)
5 4syl.4 . 2 (𝜃𝜏)
64, 5syl 17 1 (𝜑𝜏)
 Colors of variables: wff setvar class Syntax hints:   → wi 4 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7 This theorem is referenced by:  aevlem  1968  aevlemOLD  1976  aevlemALTOLD  2308  eqeq1d  2612  2reu5  3383  f1ocnvfvrneq  6441  isoselem  6491  isose  6493  fnwelem  7179  tposss  7240  wfrlem5  7306  smoiso  7346  nneob  7619  difsnen  7927  ordtypelem10  8315  oismo  8328  cantnflt2  8453  oemapso  8462  cantnf  8473  scott0  8632  tskwe  8659  infxpenlem  8719  ac10ct  8740  acndom  8757  dfac12lem2  8849  dfac12r  8851  pwcdadom  8921  ackbij1lem15  8939  ackbij2lem2  8945  ackbij2lem3  8946  ackbij2  8948  fin23lem22  9032  domtriomlem  9147  axdc3lem2  9156  sdomsdomcard  9261  canthp1lem2  9354  pwfseqlem5  9364  gchhar  9380  fzssp1  12255  fzosplitsnm1  12409  fzofzp1  12431  fzostep1  12446  bcm1k  12964  swrdccat2  13310  revccat  13366  revrev  13367  climuni  14131  isercolllem2  14244  isercoll  14246  serf0  14259  fsumparts  14379  hashiun  14395  isumsup2  14417  climcndslem1  14420  climcndslem2  14421  binomfallfaclem2  14610  oddprm  15353  vdwmc  15520  prdsplusg  15941  prdsvsca  15943  imasdsval2  15999  sscpwex  16298  ssc2  16305  pmtrfv  17695  symgtrinv  17715  odcl2  17805  lsmmod  17911  efgsdmi  17968  gsumzinv  18168  ablfac1b  18292  pgpfac1lem1  18296  pgpfaclem2  18304  ablfaclem2  18308  ablfac  18310  srng0  18683  pf1subrg  19533  mpfpf1  19536  pf1mpf  19537  znzrh2  19713  znf1o  19719  znhash  19726  znfld  19728  cygznlem3  19737  ip2di  19805  iscncl  20883  qtopcmap  21332  hmeores  21384  qtopf1  21429  fbssfi  21451  filssufil  21526  fmfnfmlem3  21570  clssubg  21722  tmsxms  22101  prdsxms  22145  metustfbas  22172  metuel2  22180  restmetu  22185  nrginvrcn  22306  nmhmcn  22728  iscmet3  22899  minveclem3  23008  ovoliunlem2  23078  ismbf3d  23227  i1fd  23254  dvadd  23509  dvmul  23510  dvaddf  23511  dvco  23516  dvcof  23517  dvcnvlem  23543  mdeglt  23629  dgrub  23794  plyremlem  23863  fta1lem  23866  fta1  23867  vieta1lem2  23870  plyexmo  23872  elaa  23875  ulmcau  23953  ulmdvlem3  23960  ppinprm  24678  chtnprm  24680  dchrzrh1  24769  dchr1  24782  dchr1re  24788  dchrptlem1  24789  dchrpt  24792  dchrsum2  24793  dchrhash  24796  rpvmasumlem  24976  rpvmasum2  25001  mudivsum  25019  f1otrg  25551  cyclnspth  26159  el2spthonot  26397  usgravd0nedg  26445  minvecolem3  27116  acunirnmpt2  28842  acunirnmpt2f  28843  orngmullt  29140  locfinref  29236  pl1cn  29329  zrhunitpreima  29350  qqhnm  29362  qqhucn  29364  ldgenpisyslem1  29553  ddemeas  29626  1stmbfm  29649  2ndmbfm  29650  omsval  29682  unveldomd  29804  probmeasb  29819  signstfvp  29974  signstres  29978  bnj1098  30108  subfacp1lem5  30420  erdsze2lem1  30439  cvmseu  30512  cvmliftlem11  30531  cvmlift3lem8  30562  cvmlift3lem9  30563  frrlem5  31028  trer  31480  meran1  31580  lukshef-ax2  31584  ordcmp  31616  wl-nfeqfb  32502  phpreu  32563  poimirlem1  32580  poimirlem9  32588  poimirlem31  32610  poimirlem32  32611  mblfinlem2  32617  sdclem2  32708  ismtyhmeolem  32773  heiborlem10  32789  lpssat  33318  lssatle  33320  lssat  33321  cdlemk45  35253  dia2dimlem9  35379  diblsmopel  35478  dochspss  35685  baerlem5blem2  36019  hdmap14lem4a  36181  aomclem6  36647  kelac1  36651  kelac2  36653  isnumbasgrplem3  36694  proot1mul  36796  stoweidlem11  38904  stoweidlem14  38907  afv0nbfvbi  39880
 Copyright terms: Public domain W3C validator