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  2056  eqeq1d  2823  2reu5  3749  f1ocnvfvrneq  7036  isoselem  7088  isose  7090  fnwelem  7819  tposss  7887  wfrlem5  7953  smoiso  7993  nneob  8273  difsnen  8593  ordtypelem10  8985  oismo  8998  cantnflt2  9130  oemapso  9139  cantnf  9150  scott0  9309  tskwe  9373  infxpenlem  9433  ac10ct  9454  acndom  9471  dfac12lem2  9564  dfac12r  9566  pwdjudom  9632  ackbij1lem15  9650  ackbij2lem2  9656  ackbij2lem3  9657  ackbij2  9659  fin23lem22  9743  domtriomlem  9858  axdc3lem2  9867  sdomsdomcard  9976  canthp1lem2  10069  pwfseqlem5  10079  xnn0lem1lt  12631  fzssp1  12944  fzosplitsnm1  13106  fzofzp1  13128  fzostep1  13147  bcm1k  13669  revrev  14123  climuni  14903  isercolllem2  15016  isercoll  15018  serf0  15031  fsumparts  15155  hashiun  15171  isumsup2  15195  climcndslem1  15198  climcndslem2  15199  binomfallfaclem2  15388  oddprm  16141  vdwmc  16308  prdsplusg  16725  prdsvsca  16727  imasdsval2  16783  sscpwex  17079  ssc2  17086  pmtrfv  18574  symgtrinv  18594  odcl2  18686  lsmmod  18795  efgsdmi  18852  gsumzinv  19059  ablfac1b  19186  pgpfac1lem1  19190  pgpfaclem2  19198  ablfaclem2  19202  ablfac  19204  srng0  19625  pf1subrg  20505  mpfpf1  20508  pf1mpf  20509  znzrh2  20686  znf1o  20692  znhash  20699  znfld  20701  cygznlem3  20710  ip2di  20779  iscncl  21871  qtopcmap  22321  hmeores  22373  qtopf1  22418  fbssfi  22439  filssufil  22514  fmfnfmlem3  22558  clssubg  22711  tmsxms  23090  prdsxms  23134  metustfbas  23161  metuel2  23169  restmetu  23174  nrginvrcn  23295  nmhmcn  23718  iscmet3  23890  minveclem3  24026  ovoliunlem2  24098  ismbf3d  24249  i1fd  24276  dvadd  24531  dvmul  24532  dvaddf  24533  dvco  24538  dvcof  24539  dvcnvlem  24567  mdeglt  24653  dgrub  24818  plyremlem  24887  fta1lem  24890  fta1  24891  vieta1lem2  24894  plyexmo  24896  elaa  24899  ulmcau  24977  ulmdvlem3  24984  ppinprm  25723  chtnprm  25725  dchrzrh1  25814  dchr1  25827  dchr1re  25833  dchrptlem1  25834  dchrpt  25837  dchrsum2  25838  dchrhash  25841  rpvmasumlem  26057  rpvmasum2  26082  mudivsum  26100  f1otrg  26651  minvecolem3  28647  acunirnmpt2  30399  acunirnmpt2f  30400  tocycfvres1  30747  tocycfvres2  30748  tocyc01  30755  cycpmconjslem2  30792  orngmullt  30877  locfinref  31100  pl1cn  31193  zrhunitpreima  31214  qqhnm  31226  qqhucn  31228  ldgenpisyslem1  31417  ddemeas  31490  1stmbfm  31513  2ndmbfm  31514  omsval  31546  unveldomd  31668  probmeasb  31683  signstres  31840  bnj1098  32050  subfacp1lem5  32426  erdsze2lem1  32445  cvmseu  32518  cvmliftlem11  32537  cvmlift3lem8  32568  cvmlift3lem9  32569  trer  33659  meran1  33754  lukshef-ax2  33758  ordcmp  33790  curryset  34252  currysetlem3  34255  wl-nfeqfb  34770  phpreu  34870  poimirlem1  34887  poimirlem9  34895  poimirlem31  34917  poimirlem32  34918  mblfinlem2  34924  sdclem2  35011  ismtyhmeolem  35076  heiborlem10  35092  lpssat  36143  lssatle  36145  lssat  36146  cdlemk45  38077  dia2dimlem9  38202  diblsmopel  38301  dochspss  38508  baerlem5blem2  38842  hdmap14lem4a  39001  aomclem6  39652  kelac1  39656  kelac2  39658  isnumbasgrplem3  39698  proot1mul  39792  stoweidlem11  42289  stoweidlem14  42292  afv0nbfvbi  43343