Theorem con2i 139

Description: A contraposition inference. Its associated inference is mt2 200. (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  194  pm3.14  997  pclem6  1027  hba1w  2047  axc4  2321  festinoALT  2674  necon2ai  2961  necon2bi  2962  eueq3  3694  ssnpss  4081  psstr  4082  elndif  4108  n0i  4315  axnulALT  5274  nfcvb  5346  zfpair  5391  epelg  5554  onxpdisj  6479  ftpg  7145  nlimsucg  7835  reldmtpos  8231  bren2  8995  sdom0OLD  9121  domunsn  9139  sdom1OLD  9249  1sdom2dom  9253  enp1iOLD  9284  alephval3  10122  cdainflem  10200  ackbij1lem18  10248  isfin4p1  10327  fincssdom  10335  fin23lem41  10364  fin17  10406  fin1a2lem7  10418  axcclem  10469  pwcfsdom  10595  canthp1lem1  10664  hargch  10685  winainflem  10705  ltxrlt  11303  xmullem2  13279  rexmul  13285  xlemul1a  13302  fzdisj  13566  lcmfunsnlem2lem2  16656  smndex1n0mnd  18888  pmtrdifellem4  19458  psgnunilem3  19475  frgpcyg  21532  dvlog2lem  26611  lgsval2lem  27268  elons2  28198  strlem1  32177  chrelat2i  32292  dfrdg4  35915  finminlem  36282  bj-nimn  36527  bj-modald  36637  finxpreclem3  37357  finxpreclem5  37359  hba1-o  38861  hlrelat2  39368  cdleme50ldil  40513  lcmineqlem23  42010  onov0suclim  43245  or3or  43994  stoweidlem14  45991  alneu  47101  2nodd  48095  elsetrecslem  49511