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  2059  eqeq1d  2740  2reu5  3688  f1ocnvfvrneq  7138  isoselem  7192  isose  7194  fnwelem  7943  tposss  8014  wfrlem5OLD  8115  smoiso  8164  nneob  8446  difsnen  8794  ordtypelem10  9216  oismo  9229  cantnflt2  9361  oemapso  9370  cantnf  9381  scott0  9575  tskwe  9639  infxpenlem  9700  ac10ct  9721  acndom  9738  dfac12lem2  9831  dfac12r  9833  pwdjudom  9903  ackbij1lem15  9921  ackbij2lem2  9927  ackbij2lem3  9928  ackbij2  9930  fin23lem22  10014  domtriomlem  10129  axdc3lem2  10138  sdomsdomcard  10247  canthp1lem2  10340  pwfseqlem5  10350  xnn0lem1lt  12907  fzssp1  13228  fzosplitsnm1  13390  fzofzp1  13412  fzostep1  13431  bcm1k  13957  revrev  14408  climuni  15189  isercolllem2  15305  isercoll  15307  serf0  15320  fsumparts  15446  hashiun  15462  isumsup2  15486  climcndslem1  15489  climcndslem2  15490  binomfallfaclem2  15678  oddprm  16439  vdwmc  16607  prdsplusg  17086  prdsvsca  17088  imasdsval2  17144  sscpwex  17444  ssc2  17451  pmtrfv  18975  symgtrinv  18995  odcl2  19087  lsmmod  19196  efgsdmi  19253  gsumzinv  19461  ablfac1b  19588  pgpfac1lem1  19592  pgpfaclem2  19600  ablfaclem2  19604  ablfac  19606  srng0  20035  znzrh2  20665  znf1o  20671  znhash  20678  znfld  20680  cygznlem3  20689  ip2di  20758  pf1subrg  21424  mpfpf1  21427  pf1mpf  21428  iscncl  22328  qtopcmap  22778  hmeores  22830  qtopf1  22875  fbssfi  22896  filssufil  22971  fmfnfmlem3  23015  clssubg  23168  tmsxms  23548  prdsxms  23592  metustfbas  23619  metuel2  23627  restmetu  23632  nrginvrcn  23762  nmhmcn  24189  iscmet3  24362  minveclem3  24498  ovoliunlem2  24572  ismbf3d  24723  i1fd  24750  dvadd  25009  dvmul  25010  dvaddf  25011  dvco  25016  dvcof  25017  dvcnvlem  25045  dgrub  25300  plyremlem  25369  fta1lem  25372  fta1  25373  vieta1lem2  25376  plyexmo  25378  elaa  25381  ulmcau  25459  ulmdvlem3  25466  ppinprm  26206  chtnprm  26208  dchrzrh1  26297  dchr1  26310  dchr1re  26316  dchrptlem1  26317  dchrpt  26320  dchrsum2  26321  dchrhash  26324  rpvmasumlem  26540  rpvmasum2  26565  mudivsum  26583  f1otrg  27136  minvecolem3  29139  acunirnmpt2  30899  acunirnmpt2f  30900  tocycfvres1  31279  tocycfvres2  31280  tocyc01  31287  cycpmconjslem2  31324  orngmullt  31410  znfermltl  31464  ply1fermltl  31572  locfinref  31693  pl1cn  31807  zrhunitpreima  31828  qqhnm  31840  qqhucn  31842  ldgenpisyslem1  32031  ddemeas  32104  1stmbfm  32127  2ndmbfm  32128  omsval  32160  unveldomd  32282  probmeasb  32297  signstres  32454  bnj1098  32663  subfacp1lem5  33046  erdsze2lem1  33065  cvmseu  33138  cvmliftlem11  33157  cvmlift3lem8  33188  cvmlift3lem9  33189  trer  34432  meran1  34527  lukshef-ax2  34531  ordcmp  34563  curryset  35062  currysetlem3  35065  wl-nfeqfb  35622  phpreu  35688  poimirlem1  35705  poimirlem9  35713  poimirlem31  35735  poimirlem32  35736  mblfinlem2  35742  sdclem2  35827  ismtyhmeolem  35889  heiborlem10  35905  lpssat  36954  lssatle  36956  lssat  36957  cdlemk45  38888  dia2dimlem9  39013  diblsmopel  39112  dochspss  39319  baerlem5blem2  39653  hdmap14lem4a  39812  aomclem6  40800  kelac1  40804  kelac2  40806  isnumbasgrplem3  40846  proot1mul  40940  stoweidlem11  43442  stoweidlem14  43445  afv0nbfvbi  44530