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  2060  eqeq1d  2800  2reu5  3697  f1ocnvfvrneq  7020  isoselem  7073  isose  7075  fnwelem  7808  tposss  7876  wfrlem5  7942  smoiso  7982  nneob  8262  difsnen  8582  ordtypelem10  8975  oismo  8988  cantnflt2  9120  oemapso  9129  cantnf  9140  scott0  9299  tskwe  9363  infxpenlem  9424  ac10ct  9445  acndom  9462  dfac12lem2  9555  dfac12r  9557  pwdjudom  9627  ackbij1lem15  9645  ackbij2lem2  9651  ackbij2lem3  9652  ackbij2  9654  fin23lem22  9738  domtriomlem  9853  axdc3lem2  9862  sdomsdomcard  9971  canthp1lem2  10064  pwfseqlem5  10074  xnn0lem1lt  12625  fzssp1  12945  fzosplitsnm1  13107  fzofzp1  13129  fzostep1  13148  bcm1k  13671  revrev  14120  climuni  14901  isercolllem2  15014  isercoll  15016  serf0  15029  fsumparts  15153  hashiun  15169  isumsup2  15193  climcndslem1  15196  climcndslem2  15197  binomfallfaclem2  15386  oddprm  16137  vdwmc  16304  prdsplusg  16723  prdsvsca  16725  imasdsval2  16781  sscpwex  17077  ssc2  17084  pmtrfv  18572  symgtrinv  18592  odcl2  18684  lsmmod  18793  efgsdmi  18850  gsumzinv  19058  ablfac1b  19185  pgpfac1lem1  19189  pgpfaclem2  19197  ablfaclem2  19201  ablfac  19203  srng0  19624  znzrh2  20237  znf1o  20243  znhash  20250  znfld  20252  cygznlem3  20261  ip2di  20330  pf1subrg  20972  mpfpf1  20975  pf1mpf  20976  iscncl  21874  qtopcmap  22324  hmeores  22376  qtopf1  22421  fbssfi  22442  filssufil  22517  fmfnfmlem3  22561  clssubg  22714  tmsxms  23093  prdsxms  23137  metustfbas  23164  metuel2  23172  restmetu  23177  nrginvrcn  23298  nmhmcn  23725  iscmet3  23897  minveclem3  24033  ovoliunlem2  24107  ismbf3d  24258  i1fd  24285  dvadd  24543  dvmul  24544  dvaddf  24545  dvco  24550  dvcof  24551  dvcnvlem  24579  mdeglt  24666  dgrub  24831  plyremlem  24900  fta1lem  24903  fta1  24904  vieta1lem2  24907  plyexmo  24909  elaa  24912  ulmcau  24990  ulmdvlem3  24997  ppinprm  25737  chtnprm  25739  dchrzrh1  25828  dchr1  25841  dchr1re  25847  dchrptlem1  25848  dchrpt  25851  dchrsum2  25852  dchrhash  25855  rpvmasumlem  26071  rpvmasum2  26096  mudivsum  26114  f1otrg  26665  minvecolem3  28659  acunirnmpt2  30423  acunirnmpt2f  30424  tocycfvres1  30802  tocycfvres2  30803  tocyc01  30810  cycpmconjslem2  30847  orngmullt  30933  locfinref  31194  pl1cn  31308  zrhunitpreima  31329  qqhnm  31341  qqhucn  31343  ldgenpisyslem1  31532  ddemeas  31605  1stmbfm  31628  2ndmbfm  31629  omsval  31661  unveldomd  31783  probmeasb  31798  signstres  31955  bnj1098  32165  subfacp1lem5  32544  erdsze2lem1  32563  cvmseu  32636  cvmliftlem11  32655  cvmlift3lem8  32686  cvmlift3lem9  32687  trer  33777  meran1  33872  lukshef-ax2  33876  ordcmp  33908  curryset  34381  currysetlem3  34384  wl-nfeqfb  34941  phpreu  35041  poimirlem1  35058  poimirlem9  35066  poimirlem31  35088  poimirlem32  35089  mblfinlem2  35095  sdclem2  35180  ismtyhmeolem  35242  heiborlem10  35258  lpssat  36309  lssatle  36311  lssat  36312  cdlemk45  38243  dia2dimlem9  38368  diblsmopel  38467  dochspss  38674  baerlem5blem2  39008  hdmap14lem4a  39167  aomclem6  40003  kelac1  40007  kelac2  40009  isnumbasgrplem3  40049  proot1mul  40143  stoweidlem11  42653  stoweidlem14  42656  afv0nbfvbi  43707