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  998  pclem6  1028  hba1w  2051  axc4  2327  festinoALT  2676  necon2ai  2962  necon2bi  2963  eueq3  3671  ssnpss  4060  psstr  4061  elndif  4087  n0i  4294  axnulALT  5251  nfcvb  5323  zfpair  5368  epelg  5533  onxpdisj  6452  ftpg  7111  nlimsucg  7794  reldmtpos  8186  bren2  8932  domunsn  9067  1sdom2dom  9166  nelaneq  9518  alephval3  10032  cdainflem  10110  ackbij1lem18  10158  isfin4p1  10237  fincssdom  10245  fin23lem41  10274  fin17  10316  fin1a2lem7  10328  axcclem  10379  pwcfsdom  10506  canthp1lem1  10575  hargch  10596  winainflem  10616  ltxrlt  11215  xmullem2  13192  rexmul  13198  xlemul1a  13215  fzdisj  13479  lcmfunsnlem2lem2  16578  smndex1n0mnd  18849  pmtrdifellem4  19420  psgnunilem3  19437  frgpcyg  21540  dvlog2lem  26629  lgsval2lem  27286  elons2  28266  oldfib  28385  strlem1  32337  chrelat2i  32452  xoromon  35264  onvf1odlem1  35316  dfrdg4  36164  finminlem  36531  regsfromsetind  36688  regsfromunir1  36689  bj-nimn  36784  bj-modald  36912  finxpreclem3  37642  finxpreclem5  37644  suceldisj  39063  hba1-o  39267  hlrelat2  39773  cdleme50ldil  40918  lcmineqlem23  42415  onov0suclim  43625  or3or  44373  stoweidlem14  46366  alneu  47478  2nodd  48526  elsetrecslem  50052