Theorem 4syl 21

Description: Inference chaining three syllogisms syl 16. (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	|- ( ph -> ps )
4syl.2	|- ( ps -> ch )
4syl.3	|- ( ch -> th )
4syl.4	|- ( th -> ta )

Assertion

Ref	Expression
4syl	|- ( ph -> ta )

Proof of Theorem 4syl

Step	Hyp	Ref	Expression
1		4syl.1	. . 3 |- ( ph -> ps )
2		4syl.2	. . 3 |- ( ps -> ch )
3		4syl.3	. . 3 |- ( ch -> th )
4	1, 2, 3	3syl 20	. 2 |- ( ph -> th )
5		4syl.4	. 2 |- ( th -> ta )
6	4, 5	syl 16	1 |- ( ph -> ta )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  aevlem1  1947  aevlem1OLD  2066  eqeq1d  2384  2reu5  3233  f1ocnvfvrneq  6090  isoselem  6138  isose  6140  fnwelem  6814  tposss  6874  smoiso  6951  nneob  7219  difsnen  7518  ordtypelem10  7867  oismo  7880  cantnflt2  8005  oemapso  8014  cantnf  8025  cantnfclOLD  8029  cantnflt2OLD  8035  cantnfOLD  8047  mapfienOLD  8051  scott0  8217  tskwe  8244  infxpenlem  8304  ac10ct  8328  acndom  8345  dfac12lem2  8437  dfac12r  8439  pwcdadom  8509  ackbij1lem15  8527  ackbij2lem2  8533  ackbij2lem3  8534  ackbij2  8536  fin23lem22  8620  domtriomlem  8735  axdc3lem2  8744  sdomsdomcard  8848  canthp1lem2  8942  pwfseqlem5  8952  gchhar  8968  fzssp1  11648  fzosplitsnm1  11789  fzofzp1  11808  fzostep1  11821  bcm1k  12295  swrdccat2  12594  revccat  12651  revrev  12652  climuni  13377  isercolllem2  13490  isercoll  13492  serf0  13505  fsumparts  13622  hashiun  13638  isumsup2  13660  climcndslem1  13663  climcndslem2  13664  oddprm  14341  vdwmc  14498  prdsplusg  14865  prdsvsca  14867  imasdsval2  14923  sscpwex  15221  ssc2  15228  pmtrfv  16594  symgtrinv  16614  odcl2  16704  lsmmod  16810  efgsdmi  16867  gsumval3OLD  17025  gsumzinv  17085  gsumzinvOLD  17086  ablfac1b  17234  pgpfac1lem1  17238  pgpfaclem2  17246  ablfaclem2  17250  ablfac  17252  srng0  17622  mpfsubrg  18314  pf1subrg  18497  mpfpf1  18500  pf1mpf  18501  znzrh2  18675  znf1o  18681  znhash  18688  znfld  18690  cygznlem3  18699  ip2di  18767  iscncl  19856  qtopcmap  20305  hmeores  20357  qtopf1  20402  fbssfi  20423  filssufil  20498  fmfnfmlem3  20542  clssubg  20692  tmsxms  21074  prdsxms  21118  metustfbas  21154  metuel2  21167  restmetu  21175  nrginvrcn  21285  nmhmcn  21688  iscmet3  21817  minveclem3  21929  ovoliunlem2  21999  ismbf3d  22146  i1fd  22173  dvadd  22428  dvmul  22429  dvaddf  22430  dvco  22435  dvcof  22436  dvcnvlem  22462  mdeglt  22550  dgrub  22716  plyremlem  22785  fta1lem  22788  fta1  22789  vieta1lem2  22792  plyexmo  22794  elaa  22797  ulmcau  22875  ulmdvlem3  22882  ppinprm  23543  chtnprm  23545  dchrzrh1  23636  dchr1  23649  dchr1re  23655  dchrptlem1  23656  dchrpt  23659  dchrsum2  23660  dchrhash  23663  rpvmasumlem  23789  rpvmasum2  23814  mudivsum  23832  f1otrg  24295  cyclnspth  24752  el2spthonot  24991  usgravd0nedg  25039  subgores  25423  rngosn  25523  minvecolem3  25909  acunirnmpt2  27646  acunirnmpt2f  27647  orngmullt  27953  locfinref  27998  pl1cn  28091  zrhunitpreima  28112  qqhnm  28124  qqhucn  28126  ddemeas  28364  1stmbfm  28387  2ndmbfm  28388  omsval  28420  unveldomd  28537  probmeasb  28552  signstfvp  28711  signstres  28715  subfacp1lem5  28817  erdsze2lem1  28836  cvmseu  28910  cvmliftlem11  28929  cvmlift3lem8  28960  cvmlift3lem9  28961  ghomfo  29220  binomfallfaclem2  29328  wfrlem5  29512  frrlem5  29556  meran1  30029  lukshef-ax2  30033  ordcmp  30065  wl-nfeqfb  30155  mblfinlem2  30217  trer  30300  sdclem2  30401  ismtyhmeolem  30466  heiborlem10  30482  aomclem6  31171  kelac1  31175  kelac2  31177  isnumbasgrplem3  31222  proot1mul  31324  stoweidlem11  31959  stoweidlem14  31962  afv0nbfvbi  32402  bnj1098  34189  bj-aevlem1v  34667  lpssat  35151  lssatle  35153  lssat  35154  cdlemk45  37086  dia2dimlem9  37212  diblsmopel  37311  dochspss  37518  baerlem5blem2  37852  hdmap14lem4a  38014