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  995  pclem6  1025  hba1w  2051  axc4  2315  festinoALT  2671  necon3aiOLD  2967  necon2ai  2971  necon2bi  2972  eueq3  3708  ssnpss  4104  psstr  4105  elndif  4129  n0i  4334  axnulALT  5305  nfcvb  5375  zfpair  5420  epelg  5582  onxpdisj  6491  ftpg  7154  nlimsucg  7831  reldmtpos  8219  bren2  8979  sdom0OLD  9109  domunsn  9127  sdom1OLD  9243  1sdom2dom  9247  enp1iOLD  9280  alephval3  10105  cdainflem  10182  ackbij1lem18  10232  isfin4p1  10310  fincssdom  10318  fin23lem41  10347  fin17  10389  fin1a2lem7  10401  axcclem  10452  pwcfsdom  10578  canthp1lem1  10647  hargch  10668  winainflem  10688  ltxrlt  11284  xmullem2  13244  rexmul  13250  xlemul1a  13267  fzdisj  13528  lcmfunsnlem2lem2  16576  smndex1n0mnd  18793  pmtrdifellem4  19347  psgnunilem3  19364  frgpcyg  21129  dvlog2lem  26160  lgsval2lem  26810  strlem1  31503  chrelat2i  31618  dfrdg4  34923  finminlem  35203  bj-nimn  35440  bj-modald  35550  finxpreclem3  36274  finxpreclem5  36276  hba1-o  37767  hlrelat2  38274  cdleme50ldil  39419  lcmineqlem23  40916  onov0suclim  42024  or3or  42774  stoweidlem14  44730  alneu  45832  2nodd  46582  elsetrecslem  47744