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  2084  axc4  2355  festinoALT  2702  necon2ai  2988  necon2bi  2989  eueq3  3672  ssnpss  4037  psstr  4038  elndif  4072  n0i  4289  axnulALT  5262  nfcvb  5343  zfpair  5388  epelg  5557  onxpdisj  6511  ftpg  7187  nlimsucg  7880  reldmtpos  8282  bren2  9041  domunsn  9177  1sdom2dom  9276  nelaneqOLD  9627  alephval3  10219  cdainflem  10296  ackbij1lem18  10344  isfin4p1  10423  fincssdom  10431  fin23lem41  10460  fin17  10502  fin1a2lem7  10514  axcclem  10565  pwcfsdom  10698  canthp1lem1  10767  hargch  10788  winainflem  10808  ltxrlt  11410  xmullem2  13425  rexmul  13431  xlemul1a  13448  fzdisj  13715  lcmfunsnlem2lem2  16846  smndex1n0mnd  19143  pmtrdifellem4  19726  psgnunilem3  19743  frgpcyg  21912  dvlog2lem  27013  lgsval2lem  27667  elons2  28677  oldfib  28796  strlem1  32885  chrelat2i  33000  xoromon  35807  onvf1odlem1  36044  dfrdg4  36906  finminlem  37297  regsfromsetind  37518  regsfromunir1  37519  bj-nimn  37623  bj-modald  37764  finxpreclem3  38521  finxpreclem5  38523  suceldisj  39953  hba1-o  40157  hlrelat2  40663  cdleme50ldil  41808  lcmineqlem23  43304  onov0suclim  44479  or3or  45226  stoweidlem14  47239  alneu  48409  2nodd  49484  elsetrecslem  51082