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  2741  2reu5  3694  f1ocnvfvrneq  7167  isoselem  7221  isose  7223  fnwelem  7981  tposss  8052  wfrlem5OLD  8153  smoiso  8202  nneob  8495  difsnen  8849  ordtypelem10  9295  oismo  9308  cantnflt2  9440  oemapso  9449  cantnf  9460  scott0  9653  tskwe  9717  infxpenlem  9778  ac10ct  9799  acndom  9816  dfac12lem2  9909  dfac12r  9911  pwdjudom  9981  ackbij1lem15  9999  ackbij2lem2  10005  ackbij2lem3  10006  ackbij2  10008  fin23lem22  10092  domtriomlem  10207  axdc3lem2  10216  sdomsdomcard  10325  canthp1lem2  10418  pwfseqlem5  10428  xnn0lem1lt  12987  fzssp1  13308  fzosplitsnm1  13471  fzofzp1  13493  fzostep1  13512  bcm1k  14038  revrev  14489  climuni  15270  isercolllem2  15386  isercoll  15388  serf0  15401  fsumparts  15527  hashiun  15543  isumsup2  15567  climcndslem1  15570  climcndslem2  15571  binomfallfaclem2  15759  oddprm  16520  vdwmc  16688  prdsplusg  17178  prdsvsca  17180  imasdsval2  17236  sscpwex  17536  ssc2  17543  pmtrfv  19069  symgtrinv  19089  odcl2  19181  lsmmod  19290  efgsdmi  19347  gsumzinv  19555  ablfac1b  19682  pgpfac1lem1  19686  pgpfaclem2  19694  ablfaclem2  19698  ablfac  19700  srng0  20129  znzrh2  20762  znf1o  20768  znhash  20775  znfld  20777  cygznlem3  20786  ip2di  20855  pf1subrg  21523  mpfpf1  21526  pf1mpf  21527  iscncl  22429  qtopcmap  22879  hmeores  22931  qtopf1  22976  fbssfi  22997  filssufil  23072  fmfnfmlem3  23116  clssubg  23269  tmsxms  23651  prdsxms  23695  metustfbas  23722  metuel2  23730  restmetu  23735  nrginvrcn  23865  nmhmcn  24292  iscmet3  24466  minveclem3  24602  ovoliunlem2  24676  ismbf3d  24827  i1fd  24854  dvadd  25113  dvmul  25114  dvaddf  25115  dvco  25120  dvcof  25121  dvcnvlem  25149  dgrub  25404  plyremlem  25473  fta1lem  25476  fta1  25477  vieta1lem2  25480  plyexmo  25482  elaa  25485  ulmcau  25563  ulmdvlem3  25570  ppinprm  26310  chtnprm  26312  dchrzrh1  26401  dchr1  26414  dchr1re  26420  dchrptlem1  26421  dchrpt  26424  dchrsum2  26425  dchrhash  26428  rpvmasumlem  26644  rpvmasum2  26669  mudivsum  26687  f1otrg  27241  minvecolem3  29247  acunirnmpt2  31006  acunirnmpt2f  31007  tocycfvres1  31386  tocycfvres2  31387  tocyc01  31394  cycpmconjslem2  31431  orngmullt  31517  znfermltl  31571  ply1fermltl  31679  locfinref  31800  pl1cn  31914  zrhunitpreima  31937  qqhnm  31949  qqhucn  31951  ldgenpisyslem1  32140  ddemeas  32213  1stmbfm  32236  2ndmbfm  32237  omsval  32269  unveldomd  32391  probmeasb  32406  signstres  32563  bnj1098  32772  subfacp1lem5  33155  erdsze2lem1  33174  cvmseu  33247  cvmliftlem11  33266  cvmlift3lem8  33297  cvmlift3lem9  33298  trer  34514  meran1  34609  lukshef-ax2  34613  ordcmp  34645  curryset  35144  currysetlem3  35147  wl-nfeqfb  35704  phpreu  35770  poimirlem1  35787  poimirlem9  35795  poimirlem31  35817  poimirlem32  35818  mblfinlem2  35824  sdclem2  35909  ismtyhmeolem  35971  heiborlem10  35987  lpssat  37034  lssatle  37036  lssat  37037  cdlemk45  38968  dia2dimlem9  39093  diblsmopel  39192  dochspss  39399  baerlem5blem2  39733  hdmap14lem4a  39892  aomclem6  40891  kelac1  40895  kelac2  40897  isnumbasgrplem3  40937  proot1mul  41031  stoweidlem11  43559  stoweidlem14  43562  afv0nbfvbi  44654