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_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  2148  eqeq1d  2767  2reu5  3579  f1ocnvfvrneq  6737  isoselem  6787  isose  6789  fnwelem  7498  tposss  7560  wfrlem5  7627  smoiso  7667  nneob  7941  difsnen  8253  ordtypelem10  8643  oismo  8656  cantnflt2  8789  oemapso  8798  cantnf  8809  scott0  8968  tskwe  9031  infxpenlem  9091  ac10ct  9112  acndom  9129  dfac12lem2  9223  dfac12r  9225  pwcdadom  9295  ackbij1lem15  9313  ackbij2lem2  9319  ackbij2lem3  9320  ackbij2  9322  fin23lem22  9406  domtriomlem  9521  axdc3lem2  9530  sdomsdomcard  9639  canthp1lem2  9732  pwfseqlem5  9742  gchhar  9758  fzssp1  12596  fzosplitsnm1  12756  fzofzp1  12778  fzostep1  12797  bcm1k  13311  swrdccat2  13670  revccat  13804  revrev  13805  climuni  14582  isercolllem2  14695  isercoll  14697  serf0  14710  fsumparts  14836  hashiun  14852  isumsup2  14876  climcndslem1  14879  climcndslem2  14880  binomfallfaclem2  15067  oddprm  15808  vdwmc  15975  prdsplusg  16398  prdsvsca  16400  imasdsval2  16456  sscpwex  16754  ssc2  16761  pmtrfv  18149  symgtrinv  18169  odcl2  18260  lsmmod  18366  efgsdmi  18423  gsumzinv  18625  ablfac1b  18750  pgpfac1lem1  18754  pgpfaclem2  18762  ablfaclem2  18766  ablfac  18768  srng0  19143  pf1subrg  19999  mpfpf1  20002  pf1mpf  20003  znzrh2  20180  znf1o  20186  znhash  20193  znfld  20195  cygznlem3  20204  ip2di  20275  iscncl  21367  qtopcmap  21816  hmeores  21868  qtopf1  21913  fbssfi  21934  filssufil  22009  fmfnfmlem3  22053  clssubg  22205  tmsxms  22584  prdsxms  22628  metustfbas  22655  metuel2  22663  restmetu  22668  nrginvrcn  22789  nmhmcn  23212  iscmet3  23384  minveclem3  23503  ovoliunlem2  23575  ismbf3d  23726  i1fd  23753  dvadd  24008  dvmul  24009  dvaddf  24010  dvco  24015  dvcof  24016  dvcnvlem  24044  mdeglt  24130  dgrub  24295  plyremlem  24364  fta1lem  24367  fta1  24368  vieta1lem2  24371  plyexmo  24373  elaa  24376  ulmcau  24454  ulmdvlem3  24461  ppinprm  25183  chtnprm  25185  dchrzrh1  25274  dchr1  25287  dchr1re  25293  dchrptlem1  25294  dchrpt  25297  dchrsum2  25298  dchrhash  25301  rpvmasumlem  25481  rpvmasum2  25506  mudivsum  25524  f1otrg  26056  minvecolem3  28209  acunirnmpt2  29931  acunirnmpt2f  29932  orngmullt  30277  locfinref  30376  pl1cn  30469  zrhunitpreima  30490  qqhnm  30502  qqhucn  30504  ldgenpisyslem1  30694  ddemeas  30767  1stmbfm  30790  2ndmbfm  30791  omsval  30823  unveldomd  30946  probmeasb  30961  signstfvp  31119  signstres  31123  bnj1098  31323  subfacp1lem5  31635  erdsze2lem1  31654  cvmseu  31727  cvmliftlem11  31746  cvmlift3lem8  31777  cvmlift3lem9  31778  frrlem5  32249  trer  32775  meran1  32870  lukshef-ax2  32874  ordcmp  32906  wl-nfeqfb  33769  phpreu  33838  poimirlem1  33855  poimirlem9  33863  poimirlem31  33885  poimirlem32  33886  mblfinlem2  33892  sdclem2  33981  ismtyhmeolem  34046  heiborlem10  34062  lpssat  34990  lssatle  34992  lssat  34993  cdlemk45  36924  dia2dimlem9  37049  diblsmopel  37148  dochspss  37355  baerlem5blem2  37689  hdmap14lem4a  37848  aomclem6  38330  kelac1  38334  kelac2  38336  isnumbasgrplem3  38376  proot1mul  38478  stoweidlem11  40889  stoweidlem14  40892  afv0nbfvbi  41923