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  2326  festinoALT  2675  necon2ai  2961  necon2bi  2962  eueq3  3669  ssnpss  4058  psstr  4059  elndif  4085  n0i  4292  axnulALT  5249  nfcvb  5321  zfpair  5366  epelg  5525  onxpdisj  6444  ftpg  7101  nlimsucg  7784  reldmtpos  8176  bren2  8920  domunsn  9055  1sdom2dom  9154  nelaneq  9506  alephval3  10020  cdainflem  10098  ackbij1lem18  10146  isfin4p1  10225  fincssdom  10233  fin23lem41  10262  fin17  10304  fin1a2lem7  10316  axcclem  10367  pwcfsdom  10494  canthp1lem1  10563  hargch  10584  winainflem  10604  ltxrlt  11203  xmullem2  13180  rexmul  13186  xlemul1a  13203  fzdisj  13467  lcmfunsnlem2lem2  16566  smndex1n0mnd  18837  pmtrdifellem4  19408  psgnunilem3  19425  frgpcyg  21528  dvlog2lem  26617  lgsval2lem  27274  elons2  28254  oldfib  28373  strlem1  32325  chrelat2i  32440  xoromon  35245  onvf1odlem1  35297  dfrdg4  36145  finminlem  36512  regsfromsetind  36669  regsfromunir1  36670  bj-nimn  36763  bj-modald  36874  finxpreclem3  37594  finxpreclem5  37596  hba1-o  39153  hlrelat2  39659  cdleme50ldil  40804  lcmineqlem23  42301  onov0suclim  43512  or3or  44260  stoweidlem14  46254  alneu  47366  2nodd  48414  elsetrecslem  49940