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

Theorem syl6com 36
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 34 . 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  1800  ax6e  2232  axc16i  2305  rgen2a  2955  wefrc  5018  elres  5338  sorpssuni  6817  sorpssint  6818  ordzsl  6910  limuni3  6917  funcnvuni  6985  funrnex  6999  soxp  7150  wfrlem4  7278  wfrlem12  7286  oaabs  7584  eceqoveq  7713  php3  8004  pssinf  8028  unbnn2  8075  inf0  8374  inf3lem5  8385  tcel  8477  rankxpsuc  8601  carduni  8663  prdom2  8685  dfac5  8807  cflm  8928  indpi  9581  prlem934  9707  negf1o  10307  xrub  11966  injresinjlem  12401  hashgt12el  13018  hashgt12el2  13019  fi1uzind  13076  fi1uzindOLD  13082  cshwcsh2id  13367  cshwshash  15591  dfgrp2  17212  symgextf1  17606  gsummoncoe1  19437  basis2  20504  fbdmn0  21386  usgranloopv  25669  nbgranself2  25727  usgrwlknloop  25855  wlkdvspthlem  25899  4cyclusnfrgra  26308  frgrancvvdeqlem7  26325  atcv0eq  28424  dfon2lem9  30742  trpredrec  30784  frmin  30785  frrlem4  30829  frrlem11  30838  altopthsn  31040  rankeq1o  31250  bj-currypeirce  31516  wl-orel12  32272  wl-equsb4  32316  rngoueqz  32708  hbtlem5  36516  ntrk0kbimka  37156  funressnfv  39657  afvco2  39706  ndmaovcl  39733  bgoldbtbndlem4  40025  rusgr1vtxlem  40785  conngrv2edg  41360  frcond1  41436  4cyclusnfrgr  41460  frgrncvvdeqlem7  41473  rngdir  41670  zlmodzxznm  42078
  Copyright terms: Public domain W3C validator