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

Theorem con2i 133
Description: A contraposition inference. Its associated inference is mt2 190. (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 132 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  134  notnot  135  pm2.65i  184  pm3.14  522  pclem6  967  hba1w  1961  hba1wOLD  1962  axc4  2115  festino  2559  calemes  2569  fresison  2571  calemos  2572  fesapo  2573  necon3ai  2807  necon2ai  2811  necon2bi  2812  eueq3  3348  ssnpss  3672  psstr  3673  elndif  3696  n0i  3879  axnulALT  4715  nfcvb  4824  zfpair  4831  onxpdisj  5764  funtpgOLD  5857  ftpg  6328  nlimsucg  6934  reldmtpos  7247  bren2  7872  sdom0  7977  domunsn  7995  sdom1  8045  enp1i  8080  alephval3  8816  dfac2  8836  cdainflem  8896  ackbij1lem18  8942  isfin4-3  9020  fincssdom  9028  fin23lem41  9057  fin45  9097  fin17  9099  fin1a2lem7  9111  axcclem  9162  pwcfsdom  9284  canthp1lem1  9353  hargch  9374  winainflem  9394  ltxrlt  9987  xmullem2  11967  rexmul  11973  xlemul1a  11990  fzdisj  12239  lcmfunsnlem2lem2  15190  pmtrdifellem4  17722  psgnunilem3  17739  frgpcyg  19741  dvlog2lem  24198  lgsval2lem  24832  isusgra0  25876  usgraop  25879  cusgrares  26001  2pthlem2  26126  2spot0  26591  strlem1  28493  chrelat2i  28608  dfrdg4  31228  finminlem  31482  bj-nimn  31721  bj-modald  31848  finxpreclem3  32406  finxpreclem5  32408  hba1-o  33200  hlrelat2  33707  cdleme50ldil  34854  or3or  37339  stoweidlem14  38907  alneu  39850  2nodd  41602  elsetrecslem  42243
  Copyright terms: Public domain W3C validator