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 ⊢ (𝜓 → ¬ 𝜑)

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  141  notnot  143  pm2.65iOLD  197  pm3.14  1011  pclem6  1041  hba1w  2072  axc4  2356  festinoALT  2704  necon2ai  2989  necon2bi  2990  eueq3  3677  ssnpss  4063  psstr  4064  elndif  4089  n0i  4295  axnulALT  5259  nfcvb  5338  zfpair  5383  epelg  5553  onxpdisj  6477  ftpg  7143  nlimsucg  7826  reldmtpos  8218  bren2  8968  domunsn  9103  1sdom2dom  9202  nelaneqOLD  9553  alephval3  10082  cdainflem  10159  ackbij1lem18  10207  isfin4p1  10287  fincssdom  10295  fin23lem41  10324  fin17  10366  fin1a2lem7  10378  axcclem  10429  pwcfsdom  10556  canthp1lem1  10625  hargch  10646  winainflem  10666  ltxrlt  11268  xmullem2  13282  rexmul  13288  xlemul1a  13305  fzdisj  13570  lcmfunsnlem2lem2  16687  smndex1n0mnd  18964  pmtrdifellem4  19540  psgnunilem3  19557  frgpcyg  21683  dvlog2lem  26775  lgsval2lem  27429  elons2  28409  oldfib  28528  strlem1  32511  chrelat2i  32626  xoromon  35394  onvf1odlem1  35458  dfrdg4  36314  finminlem  36691  regsfromsetind  36912  regsfromunir1  36913  bj-nimn  37017  bj-modald  37158  finxpreclem3  37899  finxpreclem5  37901  suceldisj  39329  hba1-o  39533  hlrelat2  40039  cdleme50ldil  41184  lcmineqlem23  42680  onov0suclim  43863  or3or  44611  stoweidlem14  46586  alneu  47716  2nodd  48792  elsetrecslem  50328