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  2735  2reu5  3755  f1ocnvfvrneq  7284  isoselem  7338  isose  7340  fnwelem  8117  tposss  8212  wfrlem5OLD  8313  smoiso  8362  nneob  8655  difsnen  9053  ordtypelem10  9522  oismo  9535  cantnflt2  9668  oemapso  9677  cantnf  9688  scott0  9881  tskwe  9945  infxpenlem  10008  ac10ct  10029  acndom  10046  dfac12lem2  10139  dfac12r  10141  pwdjudom  10211  ackbij1lem15  10229  ackbij2lem2  10235  ackbij2lem3  10236  ackbij2  10238  fin23lem22  10322  domtriomlem  10437  axdc3lem2  10446  sdomsdomcard  10555  canthp1lem2  10648  pwfseqlem5  10658  xnn0lem1lt  13223  fzssp1  13544  fzosplitsnm1  13707  fzofzp1  13729  fzostep1  13748  bcm1k  14275  revrev  14717  climuni  15496  isercolllem2  15612  isercoll  15614  serf0  15627  fsumparts  15752  hashiun  15768  isumsup2  15792  climcndslem1  15795  climcndslem2  15796  binomfallfaclem2  15984  oddprm  16743  vdwmc  16911  prdsplusg  17404  prdsvsca  17406  imasdsval2  17462  sscpwex  17762  ssc2  17769  pmtrfv  19320  symgtrinv  19340  odcl2  19433  lsmmod  19543  efgsdmi  19600  gsumzinv  19813  ablfac1b  19940  pgpfac1lem1  19944  pgpfaclem2  19952  ablfaclem2  19956  ablfac  19958  srng0  20468  znzrh2  21101  znf1o  21107  znhash  21114  znfld  21116  cygznlem3  21125  ip2di  21194  pf1subrg  21867  mpfpf1  21870  pf1mpf  21871  iscncl  22773  qtopcmap  23223  hmeores  23275  qtopf1  23320  fbssfi  23341  filssufil  23416  fmfnfmlem3  23460  clssubg  23613  tmsxms  23995  prdsxms  24039  metustfbas  24066  metuel2  24074  restmetu  24079  nrginvrcn  24209  nmhmcn  24636  iscmet3  24810  minveclem3  24946  ovoliunlem2  25020  ismbf3d  25171  i1fd  25198  dvadd  25457  dvmul  25458  dvaddf  25459  dvco  25464  dvcof  25465  dvcnvlem  25493  dgrub  25748  plyremlem  25817  fta1lem  25820  fta1  25821  vieta1lem2  25824  plyexmo  25826  elaa  25829  ulmcau  25907  ulmdvlem3  25914  ppinprm  26656  chtnprm  26658  dchrzrh1  26747  dchr1  26760  dchr1re  26766  dchrptlem1  26767  dchrpt  26770  dchrsum2  26771  dchrhash  26774  rpvmasumlem  26990  rpvmasum2  27015  mudivsum  27033  f1otrg  28122  minvecolem3  30129  acunirnmpt2  31885  acunirnmpt2f  31886  tocycfvres1  32269  tocycfvres2  32270  tocyc01  32277  cycpmconjslem2  32314  orngmullt  32427  znfermltl  32479  qusrn  32520  ply1fermltl  32663  locfinref  32821  pl1cn  32935  zrhunitpreima  32958  qqhnm  32970  qqhucn  32972  ldgenpisyslem1  33161  ddemeas  33234  1stmbfm  33259  2ndmbfm  33260  omsval  33292  unveldomd  33414  probmeasb  33429  signstres  33586  bnj1098  33794  subfacp1lem5  34175  erdsze2lem1  34194  cvmseu  34267  cvmliftlem11  34286  cvmlift3lem8  34317  cvmlift3lem9  34318  trer  35201  meran1  35296  lukshef-ax2  35300  ordcmp  35332  curryset  35827  currysetlem3  35830  wl-nfeqfb  36405  phpreu  36472  poimirlem1  36489  poimirlem9  36497  poimirlem31  36519  poimirlem32  36520  mblfinlem2  36526  sdclem2  36610  ismtyhmeolem  36672  heiborlem10  36688  lpssat  37883  lssatle  37885  lssat  37886  cdlemk45  39818  dia2dimlem9  39943  diblsmopel  40042  dochspss  40249  baerlem5blem2  40583  hdmap14lem4a  40742  aomclem6  41801  kelac1  41805  kelac2  41807  isnumbasgrplem3  41847  proot1mul  41941  stoweidlem11  44727  stoweidlem14  44730  afv0nbfvbi  45859