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  2050  axc4  2322  festinoALT  2670  necon2ai  2957  necon2bi  2958  eueq3  3670  ssnpss  4056  psstr  4057  elndif  4083  n0i  4290  axnulALT  5242  nfcvb  5314  zfpair  5359  epelg  5517  onxpdisj  6433  ftpg  7089  nlimsucg  7772  reldmtpos  8164  bren2  8905  domunsn  9040  1sdom2dom  9138  nelaneq  9487  alephval3  9998  cdainflem  10076  ackbij1lem18  10124  isfin4p1  10203  fincssdom  10211  fin23lem41  10240  fin17  10282  fin1a2lem7  10294  axcclem  10345  pwcfsdom  10471  canthp1lem1  10540  hargch  10561  winainflem  10581  ltxrlt  11180  xmullem2  13161  rexmul  13167  xlemul1a  13184  fzdisj  13448  lcmfunsnlem2lem2  16547  smndex1n0mnd  18817  pmtrdifellem4  19389  psgnunilem3  19406  frgpcyg  21508  dvlog2lem  26586  lgsval2lem  27243  elons2  28193  strlem1  32225  chrelat2i  32340  onvf1odlem1  35135  dfrdg4  35984  finminlem  36351  bj-nimn  36596  bj-modald  36706  finxpreclem3  37426  finxpreclem5  37428  hba1-o  38935  hlrelat2  39441  cdleme50ldil  40586  lcmineqlem23  42083  onov0suclim  43306  or3or  44055  stoweidlem14  46051  alneu  47154  2nodd  48202  elsetrecslem  49730