Theorem con2i 140

Description: A contraposition inference. Its associated inference is mt2 203. (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

Step	Hyp	Ref	Expression
1		con2i.a	. 2 ⊢ (𝜑 → ¬ 𝜓)
2		id 23	. 2 ⊢ (𝜓 → 𝜓)
3	1, 2	nsyl3 139	1 ⊢ (𝜓 → ¬ 𝜑)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  nsyl  141  notnot  143  pm2.65iOLD  197  pm3.14  1011  pclem6  1043  hba1w  2082  axc4  2352  festinoALT  2700  necon2ai  2985  necon2bi  2986  eueq3  3669  ssnpss  4055  psstr  4056  elndif  4080  n0i  4286  axnulALT  5258  nfcvb  5338  zfpair  5383  epelg  5552  onxpdisj  6490  ftpg  7160  nlimsucg  7853  reldmtpos  8251  bren2  9010  domunsn  9146  1sdom2dom  9245  nelaneqOLD  9597  alephval3  10189  cdainflem  10266  ackbij1lem18  10314  isfin4p1  10393  fincssdom  10401  fin23lem41  10430  fin17  10472  fin1a2lem7  10484  axcclem  10535  pwcfsdom  10668  canthp1lem1  10737  hargch  10758  winainflem  10778  ltxrlt  11380  xmullem2  13395  rexmul  13401  xlemul1a  13418  fzdisj  13685  lcmfunsnlem2lem2  16814  smndex1n0mnd  19111  pmtrdifellem4  19693  psgnunilem3  19710  frgpcyg  21879  dvlog2lem  26980  lgsval2lem  27634  elons2  28644  oldfib  28763  strlem1  32852  chrelat2i  32967  xoromon  35716  onvf1odlem1  35882  dfrdg4  36715  finminlem  37106  regsfromsetind  37327  regsfromunir1  37328  bj-nimn  37432  bj-modald  37573  finxpreclem3  38316  finxpreclem5  38318  suceldisj  39750  hba1-o  39954  hlrelat2  40460  cdleme50ldil  41605  lcmineqlem23  43101  onov0suclim  44275  or3or  45022  stoweidlem14  47023  alneu  48193  2nodd  49268  elsetrecslem  50791