Theorem con2i 140

Description: A contraposition inference. Its associated inference is mt2 203. (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 23	. 2 ⊢ (𝜓 → 𝜓)
3	1, 2	nsyl3 139	1 ⊢ (𝜓 → ¬ 𝜑)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  nsyl  141  notnot  143  pm2.65iOLD  197  pm3.14  1011  pclem6  1043  hba1w  2082  axc4  2352  festinoALT  2700  necon2ai  2985  necon2bi  2986  eueq3  3669  ssnpss  4055  psstr  4056  elndif  4080  n0i  4286  axnulALT  5258  nfcvb  5338  zfpair  5383  epelg  5552  onxpdisj  6483  ftpg  7152  nlimsucg  7842  reldmtpos  8235  bren2  8994  domunsn  9130  1sdom2dom  9229  nelaneqOLD  9581  alephval3  10170  cdainflem  10247  ackbij1lem18  10295  isfin4p1  10374  fincssdom  10382  fin23lem41  10411  fin17  10453  fin1a2lem7  10465  axcclem  10516  pwcfsdom  10649  canthp1lem1  10718  hargch  10739  winainflem  10759  ltxrlt  11361  xmullem2  13376  rexmul  13382  xlemul1a  13399  fzdisj  13665  lcmfunsnlem2lem2  16794  smndex1n0mnd  19091  pmtrdifellem4  19673  psgnunilem3  19690  frgpcyg  21859  dvlog2lem  26962  lgsval2lem  27616  elons2  28626  oldfib  28745  strlem1  32834  chrelat2i  32949  xoromon  35697  onvf1odlem1  35855  dfrdg4  36685  finminlem  37076  regsfromsetind  37297  regsfromunir1  37298  bj-nimn  37402  bj-modald  37543  finxpreclem3  38284  finxpreclem5  38286  suceldisj  39718  hba1-o  39922  hlrelat2  40428  cdleme50ldil  41573  lcmineqlem23  43069  onov0suclim  44234  or3or  44982  stoweidlem14  46968  alneu  48138  2nodd  49213  elsetrecslem  50736