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  2353  festinoALT  2701  necon2ai  2986  necon2bi  2987  eueq3  3672  ssnpss  4058  psstr  4059  elndif  4083  n0i  4289  axnulALT  5265  nfcvb  5345  zfpair  5390  epelg  5560  onxpdisj  6489  ftpg  7157  nlimsucg  7842  reldmtpos  8236  bren2  8993  domunsn  9129  1sdom2dom  9228  nelaneqOLD  9579  alephval3  10117  cdainflem  10194  ackbij1lem18  10242  isfin4p1  10321  fincssdom  10329  fin23lem41  10358  fin17  10400  fin1a2lem7  10412  axcclem  10463  pwcfsdom  10596  canthp1lem1  10665  hargch  10686  winainflem  10706  ltxrlt  11308  xmullem2  13321  rexmul  13327  xlemul1a  13344  fzdisj  13610  lcmfunsnlem2lem2  16735  smndex1n0mnd  19030  pmtrdifellem4  19612  psgnunilem3  19629  frgpcyg  21792  dvlog2lem  26897  lgsval2lem  27551  elons2  28531  oldfib  28650  strlem1  32739  chrelat2i  32854  xoromon  35601  onvf1odlem1  35708  dfrdg4  36538  finminlem  36945  regsfromsetind  37166  regsfromunir1  37167  bj-nimn  37271  bj-modald  37412  finxpreclem3  38155  finxpreclem5  38157  suceldisj  39574  hba1-o  39778  hlrelat2  40284  cdleme50ldil  41429  lcmineqlem23  42925  onov0suclim  44123  or3or  44871  stoweidlem14  46850  alneu  48020  2nodd  49095  elsetrecslem  50633