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  2357  festinoALT  2705  necon2ai  2990  necon2bi  2991  eueq3  3677  ssnpss  4064  psstr  4065  elndif  4090  n0i  4296  axnulALT  5272  nfcvb  5352  zfpair  5397  epelg  5567  onxpdisj  6495  ftpg  7160  nlimsucg  7847  reldmtpos  8239  bren2  8989  domunsn  9125  1sdom2dom  9224  nelaneqOLD  9575  alephval3  10113  cdainflem  10190  ackbij1lem18  10238  isfin4p1  10317  fincssdom  10325  fin23lem41  10354  fin17  10396  fin1a2lem7  10408  axcclem  10459  pwcfsdom  10586  canthp1lem1  10655  hargch  10676  winainflem  10696  ltxrlt  11298  xmullem2  13309  rexmul  13315  xlemul1a  13332  fzdisj  13598  lcmfunsnlem2lem2  16722  smndex1n0mnd  19005  pmtrdifellem4  19580  psgnunilem3  19597  frgpcyg  21760  dvlog2lem  26854  lgsval2lem  27508  elons2  28488  oldfib  28607  strlem1  32639  chrelat2i  32754  xoromon  35504  onvf1odlem1  35611  dfrdg4  36464  finminlem  36870  regsfromsetind  37091  regsfromunir1  37092  bj-nimn  37196  bj-modald  37337  finxpreclem3  38080  finxpreclem5  38082  suceldisj  39508  hba1-o  39712  hlrelat2  40218  cdleme50ldil  41363  lcmineqlem23  42859  onov0suclim  44042  or3or  44790  stoweidlem14  46769  alneu  47902  2nodd  48978  elsetrecslem  50518