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  1810  ax6e  2249  axc16i  2321  rgen2a  2973  wefrc  5078  elres  5404  sorpssuni  6911  sorpssint  6912  ordzsl  7007  limuni3  7014  funcnvuni  7081  funrnex  7095  soxp  7250  wfrlem4  7378  wfrlem12  7386  oaabs  7684  eceqoveq  7813  php3  8106  pssinf  8130  unbnn2  8177  inf0  8478  inf3lem5  8489  tcel  8581  rankxpsuc  8705  carduni  8767  prdom2  8789  dfac5  8911  cflm  9032  indpi  9689  prlem934  9815  negf1o  10420  xrub  12101  injresinjlem  12544  hashgt12el  13166  hashgt12el2  13167  fi1uzind  13234  fi1uzindOLD  13240  cshwcsh2id  13527  cshwshash  15754  dfgrp2  17387  symgextf1  17781  gsummoncoe1  19614  basis2  20695  fbdmn0  21578  rusgr1vtxlem  26387  conngrv2edg  26955  frcond1  27030  4cyclusnfrgr  27054  frgrncvvdeqlem7  27067  atcv0eq  29126  dfon2lem9  31450  trpredrec  31492  frmin  31493  frrlem4  31537  frrlem11  31546  altopthsn  31763  rankeq1o  31973  bj-currypeirce  32239  wl-orel12  32965  wl-equsb4  33009  rngoueqz  33410  hbtlem5  37218  ntrk0kbimka  37858  funressnfv  40542  afvco2  40590  ndmaovcl  40617  bgoldbtbndlem4  41015  rngdir  41200  zlmodzxznm  41604
  Copyright terms: Public domain W3C validator