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  2326  festinoALT  2675  necon2ai  2961  necon2bi  2962  eueq3  3657  ssnpss  4046  psstr  4047  elndif  4073  n0i  4280  axnulALT  5239  nfcvb  5318  zfpair  5363  epelg  5532  onxpdisj  6450  ftpg  7110  nlimsucg  7793  reldmtpos  8184  bren2  8930  domunsn  9065  1sdom2dom  9164  nelaneqOLD  9517  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  11216  xmullem2  13217  rexmul  13223  xlemul1a  13240  fzdisj  13505  lcmfunsnlem2lem2  16608  smndex1n0mnd  18883  pmtrdifellem4  19454  psgnunilem3  19471  frgpcyg  21553  dvlog2lem  26616  lgsval2lem  27270  elons2  28250  oldfib  28369  strlem1  32321  chrelat2i  32436  xoromon  35232  onvf1odlem1  35285  dfrdg4  36133  finminlem  36500  regsfromsetind  36721  regsfromunir1  36722  bj-nimn  36827  bj-modald  36968  finxpreclem3  37709  finxpreclem5  37711  suceldisj  39139  hba1-o  39343  hlrelat2  39849  cdleme50ldil  40994  lcmineqlem23  42490  onov0suclim  43702  or3or  44450  stoweidlem14  46442  alneu  47572  2nodd  48648  elsetrecslem  50174