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 Metamath program "MM-PA> MINIMIZE__WITH *" command to have very long run times. However, feel free to use "MM-PA> MINIMIZE__WITH 4syl / OVERRIDE" if you wish. Remember to update the "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

Step	Hyp	Ref	Expression
1		4syl.1	. . 3 ⊢ (𝜑 → 𝜓)
2		4syl.2	. . 3 ⊢ (𝜓 → 𝜒)
3		4syl.3	. . 3 ⊢ (𝜒 → 𝜃)
4	1, 2, 3	3syl 18	. 2 ⊢ (𝜑 → 𝜃)
5		4syl.4	. 2 ⊢ (𝜃 → 𝜏)
6	4, 5	syl 17	1 ⊢ (𝜑 → 𝜏)

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  2005  eqeq1d  2775  2reu5  3653  f1ocnvfvrneq  6866  isoselem  6916  isose  6918  fnwelem  7629  tposss  7695  wfrlem5  7762  smoiso  7802  nneob  8078  difsnen  8394  ordtypelem10  8785  oismo  8798  cantnflt2  8929  oemapso  8938  cantnf  8949  scott0  9108  tskwe  9172  infxpenlem  9232  ac10ct  9253  acndom  9270  dfac12lem2  9363  dfac12r  9365  pwdjudom  9435  ackbij1lem15  9453  ackbij2lem2  9459  ackbij2lem3  9460  ackbij2  9462  fin23lem22  9546  domtriomlem  9661  axdc3lem2  9670  sdomsdomcard  9779  canthp1lem2  9872  pwfseqlem5  9882  fzssp1  12765  fzosplitsnm1  12926  fzofzp1  12948  fzostep1  12967  bcm1k  13489  swrdccat2  13850  revccat  13984  revrev  13985  climuni  14769  isercolllem2  14882  isercoll  14884  serf0  14897  fsumparts  15020  hashiun  15036  isumsup2  15060  climcndslem1  15063  climcndslem2  15064  binomfallfaclem2  15253  oddprm  16002  vdwmc  16169  prdsplusg  16586  prdsvsca  16588  imasdsval2  16644  sscpwex  16956  ssc2  16963  pmtrfv  18354  symgtrinv  18374  odcl2  18466  lsmmod  18572  efgsdmi  18629  gsumzinv  18831  ablfac1b  18955  pgpfac1lem1  18959  pgpfaclem2  18967  ablfaclem2  18971  ablfac  18973  srng0  19366  pf1subrg  20229  mpfpf1  20232  pf1mpf  20233  znzrh2  20410  znf1o  20416  znhash  20423  znfld  20425  cygznlem3  20434  ip2di  20503  iscncl  21597  qtopcmap  22047  hmeores  22099  qtopf1  22144  fbssfi  22165  filssufil  22240  fmfnfmlem3  22284  clssubg  22436  tmsxms  22815  prdsxms  22859  metustfbas  22886  metuel2  22894  restmetu  22899  nrginvrcn  23020  nmhmcn  23443  iscmet3  23615  minveclem3  23751  ovoliunlem2  23823  ismbf3d  23974  i1fd  24001  dvadd  24256  dvmul  24257  dvaddf  24258  dvco  24263  dvcof  24264  dvcnvlem  24292  mdeglt  24378  dgrub  24543  plyremlem  24612  fta1lem  24615  fta1  24616  vieta1lem2  24619  plyexmo  24621  elaa  24624  ulmcau  24702  ulmdvlem3  24709  ppinprm  25447  chtnprm  25449  dchrzrh1  25538  dchr1  25551  dchr1re  25557  dchrptlem1  25558  dchrpt  25561  dchrsum2  25562  dchrhash  25565  rpvmasumlem  25781  rpvmasum2  25806  mudivsum  25824  f1otrg  26376  minvecolem3  28447  acunirnmpt2  30185  acunirnmpt2f  30186  xnn0lem1lt  30272  orngmullt  30594  locfinref  30782  pl1cn  30875  zrhunitpreima  30896  qqhnm  30908  qqhucn  30910  ldgenpisyslem1  31100  ddemeas  31173  1stmbfm  31196  2ndmbfm  31197  omsval  31229  unveldomd  31352  probmeasb  31367  signstfvp  31521  signstres  31525  bnj1098  31736  subfacp1lem5  32049  erdsze2lem1  32068  cvmseu  32141  cvmliftlem11  32160  cvmlift3lem8  32191  cvmlift3lem9  32192  trer  33218  meran1  33312  lukshef-ax2  33316  ordcmp  33348  curryset  33785  currysetlem3  33788  wl-nfeqfb  34251  phpreu  34350  poimirlem1  34367  poimirlem9  34375  poimirlem31  34397  poimirlem32  34398  mblfinlem2  34404  sdclem2  34492  ismtyhmeolem  34557  heiborlem10  34573  lpssat  35627  lssatle  35629  lssat  35630  cdlemk45  37561  dia2dimlem9  37686  diblsmopel  37785  dochspss  37992  baerlem5blem2  38326  hdmap14lem4a  38485  aomclem6  39089  kelac1  39093  kelac2  39095  isnumbasgrplem3  39135  proot1mul  39229  stoweidlem11  41757  stoweidlem14  41760  afv0nbfvbi  42786