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  2058  eqeq1d  2740  2reu5  3692  f1ocnvfvrneq  7150  isoselem  7204  isose  7206  fnwelem  7959  tposss  8030  wfrlem5OLD  8131  smoiso  8180  nneob  8473  difsnen  8827  ordtypelem10  9273  oismo  9286  cantnflt2  9418  oemapso  9427  cantnf  9438  scott0  9654  tskwe  9718  infxpenlem  9779  ac10ct  9800  acndom  9817  dfac12lem2  9910  dfac12r  9912  pwdjudom  9982  ackbij1lem15  10000  ackbij2lem2  10006  ackbij2lem3  10007  ackbij2  10009  fin23lem22  10093  domtriomlem  10208  axdc3lem2  10217  sdomsdomcard  10326  canthp1lem2  10419  pwfseqlem5  10429  xnn0lem1lt  12988  fzssp1  13309  fzosplitsnm1  13472  fzofzp1  13494  fzostep1  13513  bcm1k  14039  revrev  14490  climuni  15271  isercolllem2  15387  isercoll  15389  serf0  15402  fsumparts  15528  hashiun  15544  isumsup2  15568  climcndslem1  15571  climcndslem2  15572  binomfallfaclem2  15760  oddprm  16521  vdwmc  16689  prdsplusg  17179  prdsvsca  17181  imasdsval2  17237  sscpwex  17537  ssc2  17544  pmtrfv  19070  symgtrinv  19090  odcl2  19182  lsmmod  19291  efgsdmi  19348  gsumzinv  19556  ablfac1b  19683  pgpfac1lem1  19687  pgpfaclem2  19695  ablfaclem2  19699  ablfac  19701  srng0  20130  znzrh2  20763  znf1o  20769  znhash  20776  znfld  20778  cygznlem3  20787  ip2di  20856  pf1subrg  21524  mpfpf1  21527  pf1mpf  21528  iscncl  22430  qtopcmap  22880  hmeores  22932  qtopf1  22977  fbssfi  22998  filssufil  23073  fmfnfmlem3  23117  clssubg  23270  tmsxms  23652  prdsxms  23696  metustfbas  23723  metuel2  23731  restmetu  23736  nrginvrcn  23866  nmhmcn  24293  iscmet3  24467  minveclem3  24603  ovoliunlem2  24677  ismbf3d  24828  i1fd  24855  dvadd  25114  dvmul  25115  dvaddf  25116  dvco  25121  dvcof  25122  dvcnvlem  25150  dgrub  25405  plyremlem  25474  fta1lem  25477  fta1  25478  vieta1lem2  25481  plyexmo  25483  elaa  25486  ulmcau  25564  ulmdvlem3  25571  ppinprm  26311  chtnprm  26313  dchrzrh1  26402  dchr1  26415  dchr1re  26421  dchrptlem1  26422  dchrpt  26425  dchrsum2  26426  dchrhash  26429  rpvmasumlem  26645  rpvmasum2  26670  mudivsum  26688  f1otrg  27242  minvecolem3  29246  acunirnmpt2  31005  acunirnmpt2f  31006  tocycfvres1  31385  tocycfvres2  31386  tocyc01  31393  cycpmconjslem2  31430  orngmullt  31516  znfermltl  31570  ply1fermltl  31678  locfinref  31799  pl1cn  31913  zrhunitpreima  31936  qqhnm  31948  qqhucn  31950  ldgenpisyslem1  32139  ddemeas  32212  1stmbfm  32235  2ndmbfm  32236  omsval  32268  unveldomd  32390  probmeasb  32405  signstres  32562  bnj1098  32771  subfacp1lem5  33154  erdsze2lem1  33173  cvmseu  33246  cvmliftlem11  33265  cvmlift3lem8  33296  cvmlift3lem9  33297  trer  34513  meran1  34608  lukshef-ax2  34612  ordcmp  34644  curryset  35143  currysetlem3  35146  wl-nfeqfb  35703  phpreu  35769  poimirlem1  35786  poimirlem9  35794  poimirlem31  35816  poimirlem32  35817  mblfinlem2  35823  sdclem2  35908  ismtyhmeolem  35970  heiborlem10  35986  lpssat  37035  lssatle  37037  lssat  37038  cdlemk45  38969  dia2dimlem9  39094  diblsmopel  39193  dochspss  39400  baerlem5blem2  39734  hdmap14lem4a  39893  aomclem6  40892  kelac1  40896  kelac2  40898  isnumbasgrplem3  40938  proot1mul  41032  stoweidlem11  43533  stoweidlem14  43536  afv0nbfvbi  44621