MPE Home 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  2023  eqeq1d  2653  2reu5  3449  f1ocnvfvrneq  6581  isoselem  6631  isose  6633  fnwelem  7337  tposss  7398  wfrlem5  7464  smoiso  7504  nneob  7777  difsnen  8083  ordtypelem10  8473  oismo  8486  cantnflt2  8608  oemapso  8617  cantnf  8628  scott0  8787  tskwe  8814  infxpenlem  8874  ac10ct  8895  acndom  8912  dfac12lem2  9004  dfac12r  9006  pwcdadom  9076  ackbij1lem15  9094  ackbij2lem2  9100  ackbij2lem3  9101  ackbij2  9103  fin23lem22  9187  domtriomlem  9302  axdc3lem2  9311  sdomsdomcard  9420  canthp1lem2  9513  pwfseqlem5  9523  gchhar  9539  fzssp1  12422  fzosplitsnm1  12582  fzofzp1  12605  fzostep1  12624  bcm1k  13142  swrdccat2  13504  revccat  13561  revrev  13562  climuni  14327  isercolllem2  14440  isercoll  14442  serf0  14455  fsumparts  14582  hashiun  14598  isumsup2  14622  climcndslem1  14625  climcndslem2  14626  binomfallfaclem2  14815  oddprm  15562  vdwmc  15729  prdsplusg  16165  prdsvsca  16167  imasdsval2  16223  sscpwex  16522  ssc2  16529  pmtrfv  17918  symgtrinv  17938  odcl2  18028  lsmmod  18134  efgsdmi  18191  gsumzinv  18391  ablfac1b  18515  pgpfac1lem1  18519  pgpfaclem2  18527  ablfaclem2  18531  ablfac  18533  srng0  18908  pf1subrg  19760  mpfpf1  19763  pf1mpf  19764  znzrh2  19942  znf1o  19948  znhash  19955  znfld  19957  cygznlem3  19966  ip2di  20034  iscncl  21121  qtopcmap  21570  hmeores  21622  qtopf1  21667  fbssfi  21688  filssufil  21763  fmfnfmlem3  21807  clssubg  21959  tmsxms  22338  prdsxms  22382  metustfbas  22409  metuel2  22417  restmetu  22422  nrginvrcn  22543  nmhmcn  22966  iscmet3  23137  minveclem3  23246  ovoliunlem2  23317  ismbf3d  23466  i1fd  23493  dvadd  23748  dvmul  23749  dvaddf  23750  dvco  23755  dvcof  23756  dvcnvlem  23784  mdeglt  23870  dgrub  24035  plyremlem  24104  fta1lem  24107  fta1  24108  vieta1lem2  24111  plyexmo  24113  elaa  24116  ulmcau  24194  ulmdvlem3  24201  ppinprm  24923  chtnprm  24925  dchrzrh1  25014  dchr1  25027  dchr1re  25033  dchrptlem1  25034  dchrpt  25037  dchrsum2  25038  dchrhash  25041  rpvmasumlem  25221  rpvmasum2  25246  mudivsum  25264  f1otrg  25796  minvecolem3  27860  acunirnmpt2  29588  acunirnmpt2f  29589  orngmullt  29937  locfinref  30036  pl1cn  30129  zrhunitpreima  30150  qqhnm  30162  qqhucn  30164  ldgenpisyslem1  30354  ddemeas  30427  1stmbfm  30450  2ndmbfm  30451  omsval  30483  unveldomd  30605  probmeasb  30620  signstfvp  30776  signstres  30780  bnj1098  30980  subfacp1lem5  31292  erdsze2lem1  31311  cvmseu  31384  cvmliftlem11  31403  cvmlift3lem8  31434  cvmlift3lem9  31435  frrlem5  31909  trer  32435  meran1  32535  lukshef-ax2  32539  ordcmp  32571  wl-nfeqfb  33453  phpreu  33523  poimirlem1  33540  poimirlem9  33548  poimirlem31  33570  poimirlem32  33571  mblfinlem2  33577  sdclem2  33668  ismtyhmeolem  33733  heiborlem10  33749  lpssat  34618  lssatle  34620  lssat  34621  cdlemk45  36552  dia2dimlem9  36678  diblsmopel  36777  dochspss  36984  baerlem5blem2  37318  hdmap14lem4a  37480  aomclem6  37946  kelac1  37950  kelac2  37952  isnumbasgrplem3  37992  proot1mul  38094  stoweidlem11  40546  stoweidlem14  40549  afv0nbfvbi  41552
  Copyright terms: Public domain W3C validator