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	|- ( 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 18	. 2 |- ( ph -> th )
5		4syl.4	. 2 |- ( th -> ta )
6	4, 5	syl 17	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  1997  aevlem1OLD  2116  eqeq1d  2431  2reu5  3286  f1ocnvfvrneq  6199  isoselem  6247  isose  6249  fnwelem  6922  tposss  6982  wfrlem5  7048  smoiso  7089  nneob  7361  difsnen  7660  ordtypelem10  8042  oismo  8055  cantnflt2  8177  oemapso  8186  cantnf  8197  scott0  8356  tskwe  8383  infxpenlem  8443  ac10ct  8463  acndom  8480  dfac12lem2  8572  dfac12r  8574  pwcdadom  8644  ackbij1lem15  8662  ackbij2lem2  8668  ackbij2lem3  8669  ackbij2  8671  fin23lem22  8755  domtriomlem  8870  axdc3lem2  8879  sdomsdomcard  8983  canthp1lem2  9077  pwfseqlem5  9087  gchhar  9103  fzssp1  11839  fzosplitsnm1  11985  fzofzp1  12005  fzostep1  12018  bcm1k  12497  swrdccat2  12799  revccat  12856  revrev  12857  climuni  13594  isercolllem2  13707  isercoll  13709  serf0  13725  fsumparts  13844  hashiun  13860  isumsup2  13882  climcndslem1  13885  climcndslem2  13886  binomfallfaclem2  14071  oddprm  14719  vdwmc  14882  prdsplusg  15306  prdsvsca  15308  imasdsval2  15364  sscpwex  15662  ssc2  15669  pmtrfv  17035  symgtrinv  17055  odcl2  17145  lsmmod  17251  efgsdmi  17308  gsumzinv  17504  ablfac1b  17629  pgpfac1lem1  17633  pgpfaclem2  17641  ablfaclem2  17645  ablfac  17647  srng0  18014  mpfsubrg  18681  pf1subrg  18862  mpfpf1  18865  pf1mpf  18866  znzrh2  19038  znf1o  19044  znhash  19051  znfld  19053  cygznlem3  19062  ip2di  19130  iscncl  20207  qtopcmap  20656  hmeores  20708  qtopf1  20753  fbssfi  20774  filssufil  20849  fmfnfmlem3  20893  clssubg  21045  tmsxms  21423  prdsxms  21467  metustfbas  21494  metuel2  21502  restmetu  21507  nrginvrcn  21616  nmhmcn  22018  iscmet3  22147  minveclem3  22255  ovoliunlem2  22325  ismbf3d  22478  i1fd  22507  dvadd  22762  dvmul  22763  dvaddf  22764  dvco  22769  dvcof  22770  dvcnvlem  22796  mdeglt  22882  dgrub  23047  plyremlem  23116  fta1lem  23119  fta1  23120  vieta1lem2  23123  plyexmo  23125  elaa  23128  ulmcau  23206  ulmdvlem3  23213  ppinprm  23933  chtnprm  23935  dchrzrh1  24026  dchr1  24039  dchr1re  24045  dchrptlem1  24046  dchrpt  24049  dchrsum2  24050  dchrhash  24053  rpvmasumlem  24179  rpvmasum2  24204  mudivsum  24222  f1otrg  24738  cyclnspth  25195  el2spthonot  25434  usgravd0nedg  25482  subgores  25868  rngosn  25968  minvecolem3  26354  acunirnmpt2  28093  acunirnmpt2f  28094  orngmullt  28402  locfinref  28498  pl1cn  28591  zrhunitpreima  28612  qqhnm  28624  qqhucn  28626  ldgenpisyslem1  28815  ddemeas  28889  1stmbfm  28912  2ndmbfm  28913  omsval  28945  unveldomd  29065  probmeasb  29080  signstfvp  29239  signstres  29243  bnj1098  29374  subfacp1lem5  29686  erdsze2lem1  29705  cvmseu  29778  cvmliftlem11  29797  cvmlift3lem8  29828  cvmlift3lem9  29829  ghomfo  30088  frrlem5  30296  trer  30748  meran1  30847  lukshef-ax2  30851  ordcmp  30883  bj-aevlem1v  31091  wl-nfeqfb  31568  phpreu  31623  poimirlem1  31635  poimirlem9  31643  poimirlem31  31665  poimirlem32  31666  mblfinlem2  31672  sdclem2  31765  ismtyhmeolem  31830  heiborlem10  31846  lpssat  32278  lssatle  32280  lssat  32281  cdlemk45  34213  dia2dimlem9  34339  diblsmopel  34438  dochspss  34645  baerlem5blem2  34979  hdmap14lem4a  35141  aomclem6  35613  kelac1  35617  kelac2  35619  isnumbasgrplem3  35660  proot1mul  35762  stoweidlem11  37430  stoweidlem14  37433  afv0nbfvbi  38033