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 Metamath program "MM-PA> 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  2051  eqeq1d  2730  2reu5  3752  f1ocnvfvrneq  7289  isoselem  7343  isose  7345  fnwelem  8130  tposss  8226  wfrlem5OLD  8327  smoiso  8376  nneob  8670  difsnen  9071  ordtypelem10  9544  oismo  9557  cantnflt2  9690  oemapso  9699  cantnf  9710  scott0  9903  tskwe  9967  infxpenlem  10030  ac10ct  10051  acndom  10068  dfac12lem2  10161  dfac12r  10163  pwdjudom  10233  ackbij1lem15  10251  ackbij2lem2  10257  ackbij2lem3  10258  ackbij2  10260  fin23lem22  10344  domtriomlem  10459  axdc3lem2  10468  sdomsdomcard  10577  canthp1lem2  10670  pwfseqlem5  10680  xnn0lem1lt  13249  fzssp1  13570  fzosplitsnm1  13733  fzofzp1  13755  fzostep1  13774  bcm1k  14300  revrev  14743  climuni  15522  isercolllem2  15638  isercoll  15640  serf0  15653  fsumparts  15778  hashiun  15794  isumsup2  15818  climcndslem1  15821  climcndslem2  15822  binomfallfaclem2  16010  oddprm  16772  vdwmc  16940  prdsplusg  17433  prdsvsca  17435  imasdsval2  17491  sscpwex  17791  ssc2  17798  pmtrfv  19400  symgtrinv  19420  odcl2  19513  lsmmod  19623  efgsdmi  19680  gsumzinv  19893  ablfac1b  20020  pgpfac1lem1  20024  pgpfaclem2  20032  ablfaclem2  20036  ablfac  20038  srng0  20733  znzrh2  21472  znf1o  21478  znhash  21485  znfld  21487  cygznlem3  21496  ip2di  21566  pf1subrg  22260  mpfpf1  22263  pf1mpf  22264  iscncl  23166  qtopcmap  23616  hmeores  23668  qtopf1  23713  fbssfi  23734  filssufil  23809  fmfnfmlem3  23853  clssubg  24006  tmsxms  24388  prdsxms  24432  metustfbas  24459  metuel2  24467  restmetu  24472  nrginvrcn  24602  nmhmcn  25040  iscmet3  25214  minveclem3  25350  ovoliunlem2  25425  ismbf3d  25576  i1fd  25603  dvadd  25864  dvmul  25865  dvaddf  25866  dvco  25872  dvcof  25873  dvcnvlem  25901  dgrub  26161  plyremlem  26232  fta1lem  26235  fta1  26236  vieta1lem2  26239  plyexmo  26241  elaa  26244  ulmcau  26324  ulmdvlem3  26331  ppinprm  27077  chtnprm  27079  dchrzrh1  27170  dchr1  27183  dchr1re  27189  dchrptlem1  27190  dchrpt  27193  dchrsum2  27194  dchrhash  27197  rpvmasumlem  27413  rpvmasum2  27438  mudivsum  27456  f1otrg  28668  minvecolem3  30679  acunirnmpt2  32439  acunirnmpt2f  32440  tocycfvres1  32825  tocycfvres2  32826  tocyc01  32833  cycpmconjslem2  32870  orngmullt  33018  znfermltl  33072  qusrn  33113  ply1fermltl  33252  locfinref  33436  pl1cn  33550  zrhunitpreima  33573  qqhnm  33585  qqhucn  33587  ldgenpisyslem1  33776  ddemeas  33849  1stmbfm  33874  2ndmbfm  33875  omsval  33907  unveldomd  34029  probmeasb  34044  signstres  34201  bnj1098  34408  subfacp1lem5  34788  erdsze2lem1  34807  cvmseu  34880  cvmliftlem11  34899  cvmlift3lem8  34930  cvmlift3lem9  34931  trer  35794  meran1  35889  lukshef-ax2  35893  ordcmp  35925  curryset  36419  currysetlem3  36422  wl-nfeqfb  36997  phpreu  37071  poimirlem1  37088  poimirlem9  37096  poimirlem31  37118  poimirlem32  37119  mblfinlem2  37125  sdclem2  37209  ismtyhmeolem  37271  heiborlem10  37287  lpssat  38479  lssatle  38481  lssat  38482  cdlemk45  40414  dia2dimlem9  40539  diblsmopel  40638  dochspss  40845  baerlem5blem2  41179  hdmap14lem4a  41338  aomclem6  42477  kelac1  42481  kelac2  42483  isnumbasgrplem3  42523  proot1mul  42616  stoweidlem11  45393  stoweidlem14  45396  afv0nbfvbi  46525

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »