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 "minimize" command to have very long run times. However, feel free to use "minimize 4syl /override" if you wish. Remember to update the Travis "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  1981  aevlemOLD  1989  aevlemALTOLD  2320  eqeq1d  2624  2reu5  3416  f1ocnvfvrneq  6541  isoselem  6591  isose  6593  fnwelem  7292  tposss  7353  wfrlem5  7419  smoiso  7459  nneob  7732  difsnen  8042  ordtypelem10  8432  oismo  8445  cantnflt2  8570  oemapso  8579  cantnf  8590  scott0  8749  tskwe  8776  infxpenlem  8836  ac10ct  8857  acndom  8874  dfac12lem2  8966  dfac12r  8968  pwcdadom  9038  ackbij1lem15  9056  ackbij2lem2  9062  ackbij2lem3  9063  ackbij2  9065  fin23lem22  9149  domtriomlem  9264  axdc3lem2  9273  sdomsdomcard  9382  canthp1lem2  9475  pwfseqlem5  9485  gchhar  9501  fzssp1  12384  fzosplitsnm1  12542  fzofzp1  12565  fzostep1  12584  bcm1k  13102  swrdccat2  13458  revccat  13515  revrev  13516  climuni  14283  isercolllem2  14396  isercoll  14398  serf0  14411  fsumparts  14538  hashiun  14554  isumsup2  14578  climcndslem1  14581  climcndslem2  14582  binomfallfaclem2  14771  oddprm  15515  vdwmc  15682  prdsplusg  16118  prdsvsca  16120  imasdsval2  16176  sscpwex  16475  ssc2  16482  pmtrfv  17872  symgtrinv  17892  odcl2  17982  lsmmod  18088  efgsdmi  18145  gsumzinv  18345  ablfac1b  18469  pgpfac1lem1  18473  pgpfaclem2  18481  ablfaclem2  18485  ablfac  18487  srng0  18860  pf1subrg  19712  mpfpf1  19715  pf1mpf  19716  znzrh2  19894  znf1o  19900  znhash  19907  znfld  19909  cygznlem3  19918  ip2di  19986  iscncl  21073  qtopcmap  21522  hmeores  21574  qtopf1  21619  fbssfi  21641  filssufil  21716  fmfnfmlem3  21760  clssubg  21912  tmsxms  22291  prdsxms  22335  metustfbas  22362  metuel2  22370  restmetu  22375  nrginvrcn  22496  nmhmcn  22920  iscmet3  23091  minveclem3  23200  ovoliunlem2  23271  ismbf3d  23421  i1fd  23448  dvadd  23703  dvmul  23704  dvaddf  23705  dvco  23710  dvcof  23711  dvcnvlem  23739  mdeglt  23825  dgrub  23990  plyremlem  24059  fta1lem  24062  fta1  24063  vieta1lem2  24066  plyexmo  24068  elaa  24071  ulmcau  24149  ulmdvlem3  24156  ppinprm  24878  chtnprm  24880  dchrzrh1  24969  dchr1  24982  dchr1re  24988  dchrptlem1  24989  dchrpt  24992  dchrsum2  24993  dchrhash  24996  rpvmasumlem  25176  rpvmasum2  25201  mudivsum  25219  f1otrg  25751  minvecolem3  27732  acunirnmpt2  29460  acunirnmpt2f  29461  orngmullt  29809  locfinref  29908  pl1cn  30001  zrhunitpreima  30022  qqhnm  30034  qqhucn  30036  ldgenpisyslem1  30226  ddemeas  30299  1stmbfm  30322  2ndmbfm  30323  omsval  30355  unveldomd  30477  probmeasb  30492  signstfvp  30648  signstres  30652  bnj1098  30854  subfacp1lem5  31166  erdsze2lem1  31185  cvmseu  31258  cvmliftlem11  31277  cvmlift3lem8  31308  cvmlift3lem9  31309  frrlem5  31784  trer  32310  meran1  32410  lukshef-ax2  32414  ordcmp  32446  wl-nfeqfb  33323  phpreu  33393  poimirlem1  33410  poimirlem9  33418  poimirlem31  33440  poimirlem32  33441  mblfinlem2  33447  sdclem2  33538  ismtyhmeolem  33603  heiborlem10  33619  lpssat  34300  lssatle  34302  lssat  34303  cdlemk45  36235  dia2dimlem9  36361  diblsmopel  36460  dochspss  36667  baerlem5blem2  37001  hdmap14lem4a  37163  aomclem6  37629  kelac1  37633  kelac2  37635  isnumbasgrplem3  37675  proot1mul  37777  stoweidlem11  40228  stoweidlem14  40231  afv0nbfvbi  41231