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  1984  ax6e  2356  axc16i  2416  rgen2a  3124  wefrc  5271  elinxp  5609  elresOLD  5611  sorpssuni  7144  sorpssint  7145  ordzsl  7243  limuni3  7250  funcnvuni  7317  funrnex  7331  soxp  7492  wfrlem4  7621  wfrlem4OLD  7622  wfrlem12  7630  oaabs  7929  eceqoveq  8056  php3  8353  pssinf  8377  unbnn2  8424  inf0  8733  inf3lem5  8744  tcel  8836  rankxpsuc  8960  carduni  9058  prdom2  9080  dfac5  9202  cflm  9325  indpi  9982  prlem934  10108  negf1o  10714  xrub  12344  injresinjlem  12796  hashgt12el  13411  hashgt12el2  13412  fi1uzind  13480  cshwcsh2id  13857  cshwshash  16085  dfgrp2  17714  symgextf1  18104  gsummoncoe1  19947  basis2  21035  fbdmn0  21917  rusgr1vtxlem  26774  clwwlknun  27386  conngrv2edg  27473  frcond1  27546  4cyclusnfrgr  27572  atcv0eq  29694  dfon2lem9  32139  trpredrec  32181  frmin  32186  frrlem4  32227  altopthsn  32512  rankeq1o  32722  bj-currypeirce  32981  wl-orel12  33727  wl-equsb4  33764  rngoueqz  34161  hbtlem5  38375  ntrk0kbimka  39011  funressnfv  41820  afvco2  41924  ndmaovcl  41951  bgoldbtbndlem4  42372  rngdir  42551  zlmodzxznm  42955
  Copyright terms: Public domain W3C validator