Theorem con2i 139

Description: A contraposition inference. Its associated inference is mt2 199. (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 22	. 2 ⊢ (𝜓 → 𝜓)
3	1, 2	nsyl3 138	1 ⊢ (𝜓 → ¬ 𝜑)

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  140  notnot  142  pm2.65i  193  pm3.14  993  pclem6  1023  hba1w  2049  axc4  2313  festinoALT  2669  necon3aiOLD  2965  necon2ai  2969  necon2bi  2970  eueq3  3707  ssnpss  4103  psstr  4104  elndif  4128  n0i  4333  axnulALT  5304  nfcvb  5374  zfpair  5419  epelg  5581  onxpdisj  6490  ftpg  7156  nlimsucg  7835  reldmtpos  8225  bren2  8985  sdom0OLD  9115  domunsn  9133  sdom1OLD  9249  1sdom2dom  9253  enp1iOLD  9286  alephval3  10111  cdainflem  10188  ackbij1lem18  10238  isfin4p1  10316  fincssdom  10324  fin23lem41  10353  fin17  10395  fin1a2lem7  10407  axcclem  10458  pwcfsdom  10584  canthp1lem1  10653  hargch  10674  winainflem  10694  ltxrlt  11291  xmullem2  13251  rexmul  13257  xlemul1a  13274  fzdisj  13535  lcmfunsnlem2lem2  16583  smndex1n0mnd  18835  pmtrdifellem4  19395  psgnunilem3  19412  frgpcyg  21439  dvlog2lem  26500  lgsval2lem  27153  elons2  28064  strlem1  31936  chrelat2i  32051  dfrdg4  35393  finminlem  35667  bj-nimn  35904  bj-modald  36014  finxpreclem3  36738  finxpreclem5  36740  hba1-o  38231  hlrelat2  38738  cdleme50ldil  39883  lcmineqlem23  41383  onov0suclim  42487  or3or  43237  stoweidlem14  45189  alneu  46291  2nodd  47009  elsetrecslem  47906