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

Theorem con2i 141
Description: A contraposition inference. Its associated inference is mt2 201. (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 140 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  142  notnot  144  pm2.65i  195  pm3.14  991  pclem6  1021  hba1w  2047  axc4  2334  festinoALT  2763  necon3ai  3046  necon2ai  3050  necon2bi  3051  eueq3  3706  ssnpss  4084  psstr  4085  elndif  4109  n0i  4303  axnulALT  5205  nfcvb  5274  zfpair  5318  epelg  5465  onxpdisj  6308  ftpg  6914  nlimsucg  7545  reldmtpos  7891  bren2  8529  sdom0  8638  domunsn  8656  sdom1  8707  enp1i  8742  alephval3  9525  cdainflem  9602  ackbij1lem18  9648  isfin4p1  9726  fincssdom  9734  fin23lem41  9763  fin17  9805  fin1a2lem7  9817  axcclem  9868  pwcfsdom  9994  canthp1lem1  10063  hargch  10084  winainflem  10104  ltxrlt  10700  xmullem2  12648  rexmul  12654  xlemul1a  12671  fzdisj  12924  lcmfunsnlem2lem2  15973  pmtrdifellem4  18527  psgnunilem3  18544  frgpcyg  20636  dvlog2lem  25148  lgsval2lem  25797  strlem1  29941  chrelat2i  30056  dfrdg4  33296  finminlem  33550  bj-nimn  33783  bj-modald  33890  finxpreclem3  34543  finxpreclem5  34545  hba1-o  35900  hlrelat2  36406  cdleme50ldil  37551  sn-dtru  38976  or3or  40236  stoweidlem14  42165  alneu  43189  2nodd  43911  elsetrecslem  44633
  Copyright terms: Public domain W3C validator