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  1043  hba1w  2079  axc4  2354  festinoALT  2702  necon2ai  2987  necon2bi  2988  eueq3  3675  ssnpss  4062  psstr  4063  elndif  4088  n0i  4294  axnulALT  5268  nfcvb  5349  zfpair  5394  epelg  5564  onxpdisj  6490  ftpg  7155  nlimsucg  7839  reldmtpos  8231  bren2  8981  domunsn  9116  1sdom2dom  9215  nelaneqOLD  9566  alephval3  10095  cdainflem  10172  ackbij1lem18  10220  isfin4p1  10300  fincssdom  10308  fin23lem41  10337  fin17  10379  fin1a2lem7  10391  axcclem  10442  pwcfsdom  10569  canthp1lem1  10638  hargch  10659  winainflem  10679  ltxrlt  11281  xmullem2  13292  rexmul  13298  xlemul1a  13315  fzdisj  13581  lcmfunsnlem2lem2  16698  smndex1n0mnd  18975  pmtrdifellem4  19550  psgnunilem3  19567  frgpcyg  21704  dvlog2lem  26798  lgsval2lem  27452  elons2  28432  oldfib  28551  strlem1  32583  chrelat2i  32698  xoromon  35460  onvf1odlem1  35568  dfrdg4  36424  finminlem  36810  regsfromsetind  37031  regsfromunir1  37032  bj-nimn  37136  bj-modald  37277  finxpreclem3  38020  finxpreclem5  38022  suceldisj  39448  hba1-o  39652  hlrelat2  40158  cdleme50ldil  41303  lcmineqlem23  42799  onov0suclim  43984  or3or  44732  stoweidlem14  46711  alneu  47844  2nodd  48920  elsetrecslem  50460