Theorem 4syl 21

Description: Inference chaining three syllogisms. 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. (Contributed by BJ, 14-Jul-2018.) (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  2007  2reu5  3182  f1ocnvfvrneq  6005  fcof1o  6012  isoselem  6047  isose  6049  fnwelem  6702  tposss  6761  smoiso  6838  nneob  7106  difsnen  7408  ordtypelem10  7756  oismo  7769  cantnflt2  7896  oemapso  7905  cantnf  7916  cantnfclOLD  7920  cantnflt2OLD  7926  cantnfOLD  7938  mapfienOLD  7942  scott0  8108  tskwe  8135  infxpenlem  8195  ac10ct  8219  acndom  8236  dfac12lem2  8328  dfac12r  8330  pwcdadom  8400  ackbij1lem15  8418  ackbij2lem2  8424  ackbij2lem3  8425  ackbij2  8427  fin23lem22  8511  domtriomlem  8626  axdc3lem2  8635  sdomsdomcard  8739  canthp1lem2  8835  pwfseqlem5  8845  gchhar  8861  fzssp1  11516  fzosplitsnm1  11623  fzofzp1  11639  fzostep1  11650  bcm1k  12106  swrdccat2  12367  revccat  12421  revrev  12422  climuni  13045  isercolllem2  13158  isercoll  13160  serf0  13173  fsumparts  13284  hashiun  13300  isumsup2  13324  climcndslem1  13327  climcndslem2  13328  oddprm  13897  vdwmc  14054  prdsplusg  14411  prdsvsca  14413  imasdsval2  14469  sscpwex  14743  ssc2  14750  pmtrfv  15973  symgtrinv  15993  odcl2  16081  lsmmod  16187  efgsdmi  16244  gsumval3OLD  16397  gsumzinv  16457  gsumzinvOLD  16458  ablfac1b  16586  pgpfac1lem1  16590  pgpfaclem2  16598  ablfaclem2  16602  ablfac  16604  srng0  16960  mpfsubrg  17633  pf1subrg  17797  mpfpf1  17800  pf1mpf  17801  znzrh2  17993  znf1o  17999  znhash  18006  znfld  18008  cygznlem3  18017  ip2di  18085  iscncl  18888  qtopcmap  19307  hmeores  19359  qtopf1  19404  fbssfi  19425  filssufil  19500  fmfnfmlem3  19544  clssubg  19694  tmsxms  20076  prdsxms  20120  metustfbas  20156  metuel2  20169  restmetu  20177  nrginvrcn  20287  nmhmcn  20690  iscmet3  20819  minveclem3  20931  ovoliunlem2  21001  ismbf3d  21147  i1fd  21174  dvadd  21429  dvmul  21430  dvaddf  21431  dvco  21436  dvcof  21437  dvcnvlem  21463  mdeglt  21551  dgrub  21717  plyremlem  21785  fta1lem  21788  fta1  21789  vieta1lem2  21792  plyexmo  21794  elaa  21797  ulmcau  21875  ulmdvlem3  21882  ppinprm  22505  chtnprm  22507  dchrzrh1  22598  dchr1  22611  dchr1re  22617  dchrptlem1  22618  dchrpt  22621  dchrsum2  22622  dchrhash  22625  rpvmasumlem  22751  rpvmasum2  22776  mudivsum  22794  f1otrg  23132  cyclnspth  23532  usgravd0nedg  23597  subgores  23806  rngosn  23906  minvecolem3  24292  orngmullt  26292  pl1cn  26400  zrhunitpreima  26422  qqhnm  26434  qqhucn  26436  ddemeas  26667  1stmbfm  26690  2ndmbfm  26691  omsval  26723  unveldomd  26813  probmeasb  26828  signstfvp  26987  signstres  26991  subfacp1lem5  27087  erdsze2lem1  27106  cvmseu  27180  cvmliftlem11  27199  cvmlift3lem8  27230  cvmlift3lem9  27231  ghomfo  27325  relexpsucr  27347  binomfallfaclem2  27558  wfrlem5  27743  frrlem5  27787  meran1  28272  lukshef-ax2  28276  ordcmp  28308  wl-nfeqfb  28385  mblfinlem2  28448  trer  28530  sdclem2  28657  ismtyhmeolem  28722  heiborlem10  28738  aomclem6  29431  kelac1  29435  kelac2  29437  isnumbasgrplem3  29480  proot1mul  29583  stoweidlem11  29825  stoweidlem14  29828  afv0nbfvbi  30076  el2spthonot  30408  bnj1098  31796  bj-aevlem1v  32274  lpssat  32677  lssatle  32679  lssat  32680  cdlemk45  34610  dia2dimlem9  34736  diblsmopel  34835  dochspss  35042  baerlem5blem2  35376  hdmap14lem4a  35538