Theorem 4syl 20

Description: Inference chaining three syllogisms syl 18. (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 19	. 2 ⊢ (𝜑 → 𝜃)
5		4syl.4	. 2 ⊢ (𝜃 → 𝜏)
6	4, 5	syl 18	1 ⊢ (𝜑 → 𝜏)

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  aevlem  2090  eqeq1d  2764  2reu5  3719  relopabi  5807  f1ocnvfvrneq  7291  fcof1oinvd  7298  isoselem  7346  isose  7348  fnwelem  8133  tposss  8229  smoiso  8355  nneob  8648  difsnen  9061  php  9205  ordtypelem10  9503  oismo  9516  cantnflt2  9656  oemapso  9665  cantnf  9676  scott0b  9880  scott0OLD  9881  tskwe  9959  infxpenlem  10020  ac10ct  10041  acndom  10058  dfac12lem2  10151  dfac12r  10153  pwdjudom  10221  ackbij1lem15  10239  ackbij2lem2  10245  ackbij2lem3  10246  ackbij2  10248  fin23lem22  10333  domtriomlem  10448  axdc3lem2  10457  sdomsdomcard  10572  fpwwe2lem8  10651  canthp1lem2  10666  pwfseqlem5  10676  xnn0lem1lt  13300  fzssp1  13626  fzosplitsnm1  13800  fzofzp1  13824  fzostep1  13846  fldiv4lem1div2uz2  13901  fsuppmapnn0fiublem  14058  fsuppmapnn0fiub  14059  bcm1k  14383  pfxccatpfx2  14810  revrev  14840  climuni  15643  isercolllem2  15757  isercoll  15759  serf0  15772  fsumparts  15897  hashiun  15913  isumsup2  15939  climcndslem1  15942  climcndslem2  15943  binomfallfaclem2  16132  2mulprm  16789  oddprm  16908  vdwmc  17076  prdsplusg  17549  prdsvsca  17551  imasdsval2  17608  catcone0  17781  sscpwex  17910  ssc2  17917  pmtrfv  19585  symgtrinv  19605  psgnprfval  19654  odcl2  19698  lsmmod  19808  efgsdmi  19865  gsumzinv  20078  ablfac1b  20205  pgpfac1lem1  20209  pgpfaclem2  20217  ablfaclem2  20221  ablfac  20223  srng0  21026  orngsqr  21038  orngmullt  21043  ofldtos  21045  rmodislmod  21120  znzrh2  21764  znf1o  21770  znhash  21777  znfld  21779  cygznlem3  21788  psgnevpmb  21806  ip2di  21860  mpofrlmd  21996  ascl0  22105  ascl1  22106  mpfsubrg  22333  gsumply1subr  22464  evls1gsumadd  22555  pf1subrg  22579  mpfpf1  22582  pf1mpf  22583  scmatsgrp1  22750  madutpos  22870  iscncl  23500  qtopcmap  23951  hmeores  24003  qtopf1  24048  fbssfi  24069  filssufil  24144  fmfnfmlem3  24188  clssubg  24341  tmsxms  24718  prdsxms  24762  metustfbas  24789  metuel2  24797  restmetu  24802  tngngp2  24884  nrginvrcn  24924  nmhmcn  25354  iscmet3  25527  minveclem3  25663  ovoliunlem2  25737  ismbf3d  25888  i1fd  25915  dvadd  26174  dvmul  26175  dvaddf  26176  dvco  26181  dvcof  26182  dvcnvlem  26210  dgrub  26467  plyn0mulidp  26518  plyremlem  26541  fta1lem  26544  fta1  26545  vieta1lem2  26550  plyexmo  26552  elaa  26555  ulmcau  26638  ulmdvlem3  26645  efabl  26795  relogbf  27036  ppinprm  27396  chtnprm  27398  dchrzrh1  27488  dchr1  27501  dchr1re  27507  dchrptlem1  27508  dchrpt  27511  dchrsum2  27512  dchrhash  27515  gausslemma2dlem0c  27602  gausslemma2dlem0e  27604  gausslemma2dlem0i  27608  gausslemma2dlem1a  27609  gausslemma2dlem7  27617  gausslemma2d  27618  rpvmasumlem  27731  rpvmasum2  27756  mudivsum  27774  nosepssdm  27930  nosupbnd2lem1  27959  nosupbnd2  27960  noinfbnd2lem1  27974  noetasuplem2  27978  noetasuplem3  27979  noetainflem2  27982  tgldimor  28852  f1otrg  29335  nbusgrvtxm1  29847  wlkp1lem2  30140  pthdlem1  30239  crctcshlem4  30296  crctcshwlkn0  30297  crctcshtrl  30299  wspthsnonn0vne  30393  eupth2eucrct  30705  eupthvdres  30723  eucrctshift  30731  eucrct2eupth1  30732  minvecolem3  31365  acunirnmpt2  33141  acunirnmpt2f  33142  fnpreimac  33151  symgfcoeu  33530  tocycfvres1  33558  tocycfvres2  33559  tocyc01  33566  cycpmconjslem1  33602  cycpmconjslem2  33603  archiabllem1a  33639  znfermltl  33809  qusrn  33846  ressply1invg  33987  ressply1sub  33988  ply1fermltl  34004  dimkerim  34145  fedgmullem2  34148  lvecendof1f1o  34151  evls1fldgencl  34188  algextdeglem5  34239  mdetlap  34350  locfinref  34359  ordtconnlem1  34442  pl1cn  34473  zrhunitpreima  34494  qqhnm  34508  qqhucn  34510  rrexttps  34524  ldgenpisyslem1  34682  ddemeas  34755  1stmbfm  34779  2ndmbfm  34780  omsval  34812  sitgclbn  34862  eulerpartgbij  34891  eulerpartlemgs2  34899  unveldomd  34934  probmeasb  34949  signstres  35091  bnj1098  35301  dfscott3  35634  usgrcyclgt2v  35732  subfacp1lem5  35771  erdsze2lem1  35790  cvmseu  35863  cvmliftlem11  35882  cvmlift3lem8  35913  cvmlift3lem9  35914  trer  36943  meran1  37038  lukshef-ax2  37042  ordcmp  37074  curryset  37698  currysetlem3  37701  bj-snsetex  37715  pibt2  38179  wl-nfeqfb  38307  phpreu  38366  poimirlem1  38378  poimirlem2  38379  poimirlem9  38386  poimirlem18  38395  poimirlem27  38404  poimirlem31  38408  poimirlem32  38409  mblfinlem2  38415  sdclem2  38500  ismtyhmeolem  38562  heiborlem10  38578  notornotel1  38851  mpobi123f  38918  lpssat  39894  lssatle  39896  lssat  39897  cdlemk45  41828  dia2dimlem9  41953  diblsmopel  42052  dochspss  42259  baerlem5blem2  42593  hdmap14lem4a  42752  lcmineqlem2  42904  aks6d1c1p2  42983  aks6d1c1p3  42984  hashscontpowcl  42994  hashscontpow  42996  aks6d1c4  42998  idomnnzpownz  43006  idomnnzgmulnz  43007  aks6d1c6lem3  43046  aks6d1c6lem5  43051  aks6d1c7lem1  43054  aomclem6  43908  kelac1  43912  kelac2  43914  isnumbasgrplem3  43954  proot1mul  44043  ntrclsk3  44918  neicvgel1  44967  ismnushort  45133  choicefi  46039  infleinflem1  46207  supcnvlimsup  46576  stoweidlem11  46847  stoweidlem14  46850  fourierdlem12  46955  fourierdlem51  46993  fourierdlem80  47022  smfresal  47624  simpcntrab  47706  adh-minim  47897  afv0nbfvbi  48047  iccelpart  48341  fmtnoprmfac2lem1  48477  perfectALTVlem1  48645  bgoldbtbndlem2  48730  cznabel  49183  mgpsumz  49300  uprcl2  50123  lanrcl  50555  ranrcl  50556