MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  4syl Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 4syl.1 . . 3 (𝜑𝜓)
2 4syl.2 . . 3 (𝜓𝜒)
3 4syl.3 . . 3 (𝜒𝜃)
41, 2, 33syl 18 . 2 (𝜑𝜃)
5 4syl.4 . 2 (𝜃𝜏)
64, 5syl 17 1 (𝜑𝜏)
Colors of variables: wff setvar class
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  2060  eqeq1d  2824  2reu5  3724  f1ocnvfvrneq  7025  isoselem  7078  isose  7080  fnwelem  7812  tposss  7880  wfrlem5  7946  smoiso  7986  nneob  8266  difsnen  8586  ordtypelem10  8979  oismo  8992  cantnflt2  9124  oemapso  9133  cantnf  9144  scott0  9303  tskwe  9367  infxpenlem  9428  ac10ct  9449  acndom  9466  dfac12lem2  9559  dfac12r  9561  pwdjudom  9627  ackbij1lem15  9645  ackbij2lem2  9651  ackbij2lem3  9652  ackbij2  9654  fin23lem22  9738  domtriomlem  9853  axdc3lem2  9862  sdomsdomcard  9971  canthp1lem2  10064  pwfseqlem5  10074  xnn0lem1lt  12625  fzssp1  12945  fzosplitsnm1  13107  fzofzp1  13129  fzostep1  13148  bcm1k  13671  revrev  14120  climuni  14900  isercolllem2  15013  isercoll  15015  serf0  15028  fsumparts  15152  hashiun  15168  isumsup2  15192  climcndslem1  15195  climcndslem2  15196  binomfallfaclem2  15385  oddprm  16136  vdwmc  16303  prdsplusg  16722  prdsvsca  16724  imasdsval2  16780  sscpwex  17076  ssc2  17083  pmtrfv  18571  symgtrinv  18591  odcl2  18683  lsmmod  18792  efgsdmi  18849  gsumzinv  19056  ablfac1b  19183  pgpfac1lem1  19187  pgpfaclem2  19195  ablfaclem2  19199  ablfac  19201  srng0  19622  znzrh2  20235  znf1o  20241  znhash  20248  znfld  20250  cygznlem3  20259  ip2di  20328  pf1subrg  20970  mpfpf1  20973  pf1mpf  20974  iscncl  21872  qtopcmap  22322  hmeores  22374  qtopf1  22419  fbssfi  22440  filssufil  22515  fmfnfmlem3  22559  clssubg  22712  tmsxms  23091  prdsxms  23135  metustfbas  23162  metuel2  23170  restmetu  23175  nrginvrcn  23296  nmhmcn  23723  iscmet3  23895  minveclem3  24031  ovoliunlem2  24105  ismbf3d  24256  i1fd  24283  dvadd  24541  dvmul  24542  dvaddf  24543  dvco  24548  dvcof  24549  dvcnvlem  24577  mdeglt  24664  dgrub  24829  plyremlem  24898  fta1lem  24901  fta1  24902  vieta1lem2  24905  plyexmo  24907  elaa  24910  ulmcau  24988  ulmdvlem3  24995  ppinprm  25735  chtnprm  25737  dchrzrh1  25826  dchr1  25839  dchr1re  25845  dchrptlem1  25846  dchrpt  25849  dchrsum2  25850  dchrhash  25853  rpvmasumlem  26069  rpvmasum2  26094  mudivsum  26112  f1otrg  26663  minvecolem3  28657  acunirnmpt2  30413  acunirnmpt2f  30414  tocycfvres1  30783  tocycfvres2  30784  tocyc01  30791  cycpmconjslem2  30828  orngmullt  30914  locfinref  31163  pl1cn  31272  zrhunitpreima  31293  qqhnm  31305  qqhucn  31307  ldgenpisyslem1  31496  ddemeas  31569  1stmbfm  31592  2ndmbfm  31593  omsval  31625  unveldomd  31747  probmeasb  31762  signstres  31919  bnj1098  32129  subfacp1lem5  32505  erdsze2lem1  32524  cvmseu  32597  cvmliftlem11  32616  cvmlift3lem8  32647  cvmlift3lem9  32648  trer  33738  meran1  33833  lukshef-ax2  33837  ordcmp  33869  curryset  34342  currysetlem3  34345  wl-nfeqfb  34899  phpreu  34999  poimirlem1  35016  poimirlem9  35024  poimirlem31  35046  poimirlem32  35047  mblfinlem2  35053  sdclem2  35138  ismtyhmeolem  35200  heiborlem10  35216  lpssat  36267  lssatle  36269  lssat  36270  cdlemk45  38201  dia2dimlem9  38326  diblsmopel  38425  dochspss  38632  baerlem5blem2  38966  hdmap14lem4a  39125  aomclem6  39933  kelac1  39937  kelac2  39939  isnumbasgrplem3  39979  proot1mul  40073  stoweidlem11  42592  stoweidlem14  42595  afv0nbfvbi  43646
  Copyright terms: Public domain W3C validator