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  2058  eqeq1d  2733  2reu5  3719  f1ocnvfvrneq  7237  isoselem  7291  isose  7293  fnwelem  8068  tposss  8163  wfrlem5OLD  8264  smoiso  8313  nneob  8607  difsnen  9004  ordtypelem10  9472  oismo  9485  cantnflt2  9618  oemapso  9627  cantnf  9638  scott0  9831  tskwe  9895  infxpenlem  9958  ac10ct  9979  acndom  9996  dfac12lem2  10089  dfac12r  10091  pwdjudom  10161  ackbij1lem15  10179  ackbij2lem2  10185  ackbij2lem3  10186  ackbij2  10188  fin23lem22  10272  domtriomlem  10387  axdc3lem2  10396  sdomsdomcard  10505  canthp1lem2  10598  pwfseqlem5  10608  xnn0lem1lt  13173  fzssp1  13494  fzosplitsnm1  13657  fzofzp1  13679  fzostep1  13698  bcm1k  14225  revrev  14667  climuni  15446  isercolllem2  15562  isercoll  15564  serf0  15577  fsumparts  15702  hashiun  15718  isumsup2  15742  climcndslem1  15745  climcndslem2  15746  binomfallfaclem2  15934  oddprm  16693  vdwmc  16861  prdsplusg  17354  prdsvsca  17356  imasdsval2  17412  sscpwex  17712  ssc2  17719  pmtrfv  19248  symgtrinv  19268  odcl2  19361  lsmmod  19471  efgsdmi  19528  gsumzinv  19736  ablfac1b  19863  pgpfac1lem1  19867  pgpfaclem2  19875  ablfaclem2  19879  ablfac  19881  srng0  20375  znzrh2  20989  znf1o  20995  znhash  21002  znfld  21004  cygznlem3  21013  ip2di  21082  pf1subrg  21751  mpfpf1  21754  pf1mpf  21755  iscncl  22657  qtopcmap  23107  hmeores  23159  qtopf1  23204  fbssfi  23225  filssufil  23300  fmfnfmlem3  23344  clssubg  23497  tmsxms  23879  prdsxms  23923  metustfbas  23950  metuel2  23958  restmetu  23963  nrginvrcn  24093  nmhmcn  24520  iscmet3  24694  minveclem3  24830  ovoliunlem2  24904  ismbf3d  25055  i1fd  25082  dvadd  25341  dvmul  25342  dvaddf  25343  dvco  25348  dvcof  25349  dvcnvlem  25377  dgrub  25632  plyremlem  25701  fta1lem  25704  fta1  25705  vieta1lem2  25708  plyexmo  25710  elaa  25713  ulmcau  25791  ulmdvlem3  25798  ppinprm  26538  chtnprm  26540  dchrzrh1  26629  dchr1  26642  dchr1re  26648  dchrptlem1  26649  dchrpt  26652  dchrsum2  26653  dchrhash  26656  rpvmasumlem  26872  rpvmasum2  26897  mudivsum  26915  f1otrg  27876  minvecolem3  29881  acunirnmpt2  31643  acunirnmpt2f  31644  tocycfvres1  32029  tocycfvres2  32030  tocyc01  32037  cycpmconjslem2  32074  orngmullt  32175  znfermltl  32227  ply1fermltl  32362  locfinref  32511  pl1cn  32625  zrhunitpreima  32648  qqhnm  32660  qqhucn  32662  ldgenpisyslem1  32851  ddemeas  32924  1stmbfm  32949  2ndmbfm  32950  omsval  32982  unveldomd  33104  probmeasb  33119  signstres  33276  bnj1098  33484  subfacp1lem5  33865  erdsze2lem1  33884  cvmseu  33957  cvmliftlem11  33976  cvmlift3lem8  34007  cvmlift3lem9  34008  trer  34864  meran1  34959  lukshef-ax2  34963  ordcmp  34995  curryset  35490  currysetlem3  35493  wl-nfeqfb  36068  phpreu  36135  poimirlem1  36152  poimirlem9  36160  poimirlem31  36182  poimirlem32  36183  mblfinlem2  36189  sdclem2  36274  ismtyhmeolem  36336  heiborlem10  36352  lpssat  37548  lssatle  37550  lssat  37551  cdlemk45  39483  dia2dimlem9  39608  diblsmopel  39707  dochspss  39914  baerlem5blem2  40248  hdmap14lem4a  40407  aomclem6  41444  kelac1  41448  kelac2  41450  isnumbasgrplem3  41490  proot1mul  41584  stoweidlem11  44372  stoweidlem14  44375  afv0nbfvbi  45503