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

Theorem syl6com 37
Description: Syllogism inference with commuted antecedents. (Contributed by NM, 25-May-2005.)
Hypotheses
Ref Expression
syl6com.1 (𝜑 → (𝜓𝜒))
syl6com.2 (𝜒𝜃)
Assertion
Ref Expression
syl6com (𝜓 → (𝜑𝜃))

Proof of Theorem syl6com
StepHypRef Expression
1 syl6com.1 . . 3 (𝜑 → (𝜓𝜒))
2 syl6com.2 . . 3 (𝜒𝜃)
31, 2syl6 35 . 2 (𝜑 → (𝜓𝜃))
43com12 32 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:  19.33b  1886  sbequ2  2251  nfeqf2  2396  ax6e  2402  axc16i  2459  mo4  2649  rgen2a  3218  wefrc  5526  elinxp  5868  sorpssuni  7443  sorpssint  7444  ordzsl  7545  limuni3  7552  funcnvuni  7622  funrnex  7641  soxp  7810  wfrlem4  7945  wfrlem12  7953  oaabs  8258  eceqoveq  8389  php3  8691  pssinf  8716  unbnn2  8763  inf0  9072  inf3lem5  9083  tcel  9175  rankxpsuc  9299  carduni  9398  prdom2  9421  dfac5  9543  cflm  9661  indpi  10318  prlem934  10444  negf1o  11059  xrub  12693  injresinjlem  13152  hashgt12el  13779  hashgt12el2  13780  fi1uzind  13851  swrdwrdsymb  14015  cshwcsh2id  14181  cshwshash  16429  lidrididd  17871  dfgrp2  18119  symgextf1  18540  gsummoncoe1  20931  basis2  21554  fbdmn0  22437  rusgr1vtxlem  27375  upgrewlkle2  27394  clwwlknun  27895  conngrv2edg  27978  frcond1  28049  4cyclusnfrgr  28075  atcv0eq  30160  dfon2lem9  33110  trpredrec  33151  frmin  33158  frrlem4  33200  altopthsn  33496  rankeq1o  33706  bj-cbvalimt  34046  bj-cbveximt  34047  wl-orel12  34878  wl-equsb4  34920  rngoueqz  35340  hbtlem5  40006  ntrk0kbimka  40679  funressnfv  43578  afvco2  43675  ndmaovcl  43702  bgoldbtbndlem4  44269  rngdir  44449  zlmodzxznm  44849
  Copyright terms: Public domain W3C validator