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  1853  ax6e  2286  axc16i  2353  rgen2a  3006  wefrc  5137  elres  5470  sorpssuni  6988  sorpssint  6989  ordzsl  7087  limuni3  7094  funcnvuni  7161  funrnex  7175  soxp  7335  wfrlem4  7463  wfrlem12  7471  oaabs  7769  eceqoveq  7895  php3  8187  pssinf  8211  unbnn2  8258  inf0  8556  inf3lem5  8567  tcel  8659  rankxpsuc  8783  carduni  8845  prdom2  8867  dfac5  8989  cflm  9110  indpi  9767  prlem934  9893  negf1o  10498  xrub  12180  injresinjlem  12628  hashgt12el  13248  hashgt12el2  13249  fi1uzind  13317  cshwcsh2id  13620  cshwshash  15858  dfgrp2  17494  symgextf1  17887  gsummoncoe1  19722  basis2  20803  fbdmn0  21685  rusgr1vtxlem  26539  clwwlknun  27087  conngrv2edg  27173  frcond1  27246  4cyclusnfrgr  27272  atcv0eq  29366  dfon2lem9  31820  trpredrec  31862  frmin  31867  frrlem4  31908  altopthsn  32193  rankeq1o  32403  bj-currypeirce  32669  wl-orel12  33424  wl-equsb4  33468  rngoueqz  33869  hbtlem5  38015  ntrk0kbimka  38654  funressnfv  41529  afvco2  41577  ndmaovcl  41604  bgoldbtbndlem4  42021  rngdir  42207  zlmodzxznm  42611
  Copyright terms: Public domain W3C validator