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

Theorem con2i 132
Description: A contraposition inference. Its associated inference is mt2 189. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Mel L. O'Cat, 28-Nov-2008.) (Proof shortened by Wolf Lammen, 13-Jun-2013.)
Hypothesis
Ref Expression
con2i.a (𝜑 → ¬ 𝜓)
Assertion
Ref Expression
con2i (𝜓 → ¬ 𝜑)

Proof of Theorem con2i
StepHypRef Expression
1 con2i.a . 2 (𝜑 → ¬ 𝜓)
2 id 22 . 2 (𝜓𝜓)
31, 2nsyl3 131 1 (𝜓 → ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  nsyl  133  notnot  134  pm2.65i  183  pm3.14  521  pclem6  966  hba1w  1923  axc4  1991  festino  2463  calemes  2473  fresison  2475  calemos  2476  fesapo  2477  necon3ai  2711  necon2ai  2715  necon2bi  2716  eueq3  3252  ssnpss  3576  psstr  3577  elndif  3600  n0i  3782  axnulALT  4613  nfcvb  4723  zfpair  4730  onssneli  5639  onxpdisj  5649  funtpgOLD  5742  ftpg  6204  nlimsucg  6809  reldmtpos  7121  bren2  7747  sdom0  7852  domunsn  7870  sdom1  7920  enp1i  7955  alephval3  8691  dfac2  8711  cdainflem  8771  ackbij1lem18  8817  isfin4-3  8895  fincssdom  8903  fin23lem41  8932  fin45  8972  fin17  8974  fin1a2lem7  8986  axcclem  9037  pwcfsdom  9159  canthp1lem1  9228  hargch  9249  winainflem  9269  ltxrlt  9857  xmullem2  11833  rexmul  11839  xlemul1a  11856  fzdisj  12106  lcmfunsnlem2lem2  15064  pmtrdifellem4  17612  psgnunilem3  17629  frgpcyg  19645  dvlog2lem  24086  lgsval2lem  24722  isusgra0  25615  usgraop  25618  cusgrares  25740  2pthlem2  25865  2spot0  26330  strlem1  28282  chrelat2i  28397  dfrdg4  31064  finminlem  31318  bj-nimn  31556  bj-modald  31683  finxpreclem3  32238  finxpreclem5  32240  hba1-o  33075  hlrelat2  33582  cdleme50ldil  34729  or3or  37221  stoweidlem14  38797  alneu  39744  2nodd  41694
  Copyright terms: Public domain W3C validator