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  1877  sbequ2  2241  nfeqf2  2388  ax6e  2394  axc16i  2453  mo4  2646  rgen2a  3229  wefrc  5543  elinxp  5884  sorpssuni  7447  sorpssint  7448  ordzsl  7548  limuni3  7555  funcnvuni  7624  funrnex  7646  soxp  7814  wfrlem4  7949  wfrlem12  7957  oaabs  8261  eceqoveq  8392  php3  8692  pssinf  8717  unbnn2  8764  inf0  9073  inf3lem5  9084  tcel  9176  rankxpsuc  9300  carduni  9399  prdom2  9421  dfac5  9543  cflm  9661  indpi  10318  prlem934  10444  negf1o  11059  xrub  12695  injresinjlem  13147  hashgt12el  13773  hashgt12el2  13774  fi1uzind  13845  swrdwrdsymb  14014  cshwcsh2id  14180  cshwshash  16428  lidrididd  17870  dfgrp2  18068  symgextf1  18480  gsummoncoe1  20402  basis2  21489  fbdmn0  22372  rusgr1vtxlem  27297  upgrewlkle2  27316  clwwlknun  27819  conngrv2edg  27902  frcond1  27973  4cyclusnfrgr  27999  atcv0eq  30084  dfon2lem9  32934  trpredrec  32975  frmin  32982  frrlem4  33024  altopthsn  33320  rankeq1o  33530  bj-cbvalimt  33870  bj-cbveximt  33871  wl-orel12  34634  wl-equsb4  34675  rngoueqz  35101  hbtlem5  39608  ntrk0kbimka  40269  funressnfv  43159  afvco2  43256  ndmaovcl  43283  bgoldbtbndlem4  43820  rngdir  44051  zlmodzxznm  44450
  Copyright terms: Public domain W3C validator