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  2825  2reu5  3751  f1ocnvfvrneq  7044  isoselem  7096  isose  7098  fnwelem  7827  tposss  7895  wfrlem5  7961  smoiso  8001  nneob  8281  difsnen  8601  ordtypelem10  8993  oismo  9006  cantnflt2  9138  oemapso  9147  cantnf  9158  scott0  9317  tskwe  9381  infxpenlem  9441  ac10ct  9462  acndom  9479  dfac12lem2  9572  dfac12r  9574  pwdjudom  9640  ackbij1lem15  9658  ackbij2lem2  9664  ackbij2lem3  9665  ackbij2  9667  fin23lem22  9751  domtriomlem  9866  axdc3lem2  9875  sdomsdomcard  9984  canthp1lem2  10077  pwfseqlem5  10087  xnn0lem1lt  12640  fzssp1  12953  fzosplitsnm1  13115  fzofzp1  13137  fzostep1  13156  bcm1k  13678  revrev  14131  climuni  14911  isercolllem2  15024  isercoll  15026  serf0  15039  fsumparts  15163  hashiun  15179  isumsup2  15203  climcndslem1  15206  climcndslem2  15207  binomfallfaclem2  15396  oddprm  16149  vdwmc  16316  prdsplusg  16733  prdsvsca  16735  imasdsval2  16791  sscpwex  17087  ssc2  17094  pmtrfv  18582  symgtrinv  18602  odcl2  18694  lsmmod  18803  efgsdmi  18860  gsumzinv  19067  ablfac1b  19194  pgpfac1lem1  19198  pgpfaclem2  19206  ablfaclem2  19210  ablfac  19212  srng0  19633  pf1subrg  20513  mpfpf1  20516  pf1mpf  20517  znzrh2  20694  znf1o  20700  znhash  20707  znfld  20709  cygznlem3  20718  ip2di  20787  iscncl  21879  qtopcmap  22329  hmeores  22381  qtopf1  22426  fbssfi  22447  filssufil  22522  fmfnfmlem3  22566  clssubg  22719  tmsxms  23098  prdsxms  23142  metustfbas  23169  metuel2  23177  restmetu  23182  nrginvrcn  23303  nmhmcn  23726  iscmet3  23898  minveclem3  24034  ovoliunlem2  24106  ismbf3d  24257  i1fd  24284  dvadd  24539  dvmul  24540  dvaddf  24541  dvco  24546  dvcof  24547  dvcnvlem  24575  mdeglt  24661  dgrub  24826  plyremlem  24895  fta1lem  24898  fta1  24899  vieta1lem2  24902  plyexmo  24904  elaa  24907  ulmcau  24985  ulmdvlem3  24992  ppinprm  25731  chtnprm  25733  dchrzrh1  25822  dchr1  25835  dchr1re  25841  dchrptlem1  25842  dchrpt  25845  dchrsum2  25846  dchrhash  25849  rpvmasumlem  26065  rpvmasum2  26090  mudivsum  26108  f1otrg  26659  minvecolem3  28655  acunirnmpt2  30407  acunirnmpt2f  30408  tocycfvres1  30754  tocycfvres2  30755  tocyc01  30762  cycpmconjslem2  30799  orngmullt  30884  locfinref  31107  pl1cn  31200  zrhunitpreima  31221  qqhnm  31233  qqhucn  31235  ldgenpisyslem1  31424  ddemeas  31497  1stmbfm  31520  2ndmbfm  31521  omsval  31553  unveldomd  31675  probmeasb  31690  signstres  31847  bnj1098  32057  subfacp1lem5  32433  erdsze2lem1  32452  cvmseu  32525  cvmliftlem11  32544  cvmlift3lem8  32575  cvmlift3lem9  32576  trer  33666  meran1  33761  lukshef-ax2  33765  ordcmp  33797  curryset  34259  currysetlem3  34262  wl-nfeqfb  34778  phpreu  34878  poimirlem1  34895  poimirlem9  34903  poimirlem31  34925  poimirlem32  34926  mblfinlem2  34932  sdclem2  35019  ismtyhmeolem  35084  heiborlem10  35100  lpssat  36151  lssatle  36153  lssat  36154  cdlemk45  38085  dia2dimlem9  38210  diblsmopel  38309  dochspss  38516  baerlem5blem2  38850  hdmap14lem4a  39009  aomclem6  39666  kelac1  39670  kelac2  39672  isnumbasgrplem3  39712  proot1mul  39806  stoweidlem11  42303  stoweidlem14  42306  afv0nbfvbi  43357