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  996  pclem6  1026  hba1w  2047  axc4  2325  festinoALT  2678  necon3aiOLD  2972  necon2ai  2976  necon2bi  2977  eueq3  3733  ssnpss  4129  psstr  4130  elndif  4156  n0i  4363  axnulALT  5322  nfcvb  5394  zfpair  5439  epelg  5600  onxpdisj  6521  ftpg  7190  nlimsucg  7879  reldmtpos  8275  bren2  9043  sdom0OLD  9175  domunsn  9193  sdom1OLD  9306  1sdom2dom  9310  enp1iOLD  9342  alephval3  10179  cdainflem  10257  ackbij1lem18  10305  isfin4p1  10384  fincssdom  10392  fin23lem41  10421  fin17  10463  fin1a2lem7  10475  axcclem  10526  pwcfsdom  10652  canthp1lem1  10721  hargch  10742  winainflem  10762  ltxrlt  11360  xmullem2  13327  rexmul  13333  xlemul1a  13350  fzdisj  13611  lcmfunsnlem2lem2  16686  smndex1n0mnd  18947  pmtrdifellem4  19521  psgnunilem3  19538  frgpcyg  21615  dvlog2lem  26712  lgsval2lem  27369  elons2  28299  strlem1  32282  chrelat2i  32397  dfrdg4  35915  finminlem  36284  bj-nimn  36529  bj-modald  36639  finxpreclem3  37359  finxpreclem5  37361  hba1-o  38853  hlrelat2  39360  cdleme50ldil  40505  lcmineqlem23  42008  onov0suclim  43236  or3or  43985  stoweidlem14  45935  alneu  47039  2nodd  47895  elsetrecslem  48791