Theorem con2i 139

Description: A contraposition inference. Its associated inference is mt2 202. (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 22	. 2 ⊢ (𝜓 → 𝜓)
3	1, 2	nsyl3 138	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  140  notnot  142  pm2.65iOLD  196  pm3.14  1008  pclem6  1038  hba1w  2068  axc4  2352  festinoALT  2700  necon2ai  2985  necon2bi  2986  eueq3  3673  ssnpss  4060  psstr  4061  elndif  4086  n0i  4292  axnulALT  5253  nfcvb  5332  zfpair  5377  epelg  5546  onxpdisj  6469  ftpg  7135  nlimsucg  7818  reldmtpos  8209  bren2  8960  domunsn  9095  1sdom2dom  9194  nelaneqOLD  9548  alephval3  10063  cdainflem  10141  ackbij1lem18  10189  isfin4p1  10269  fincssdom  10277  fin23lem41  10306  fin17  10348  fin1a2lem7  10360  axcclem  10411  pwcfsdom  10538  canthp1lem1  10607  hargch  10628  winainflem  10648  ltxrlt  11250  xmullem2  13265  rexmul  13271  xlemul1a  13288  fzdisj  13553  lcmfunsnlem2lem2  16656  smndex1n0mnd  18932  pmtrdifellem4  19502  psgnunilem3  19519  frgpcyg  21605  dvlog2lem  26694  lgsval2lem  27348  elons2  28328  oldfib  28447  strlem1  32399  chrelat2i  32514  xoromon  35348  onvf1odlem1  35410  dfrdg4  36265  finminlem  36642  regsfromsetind  36863  regsfromunir1  36864  bj-nimn  36969  bj-modald  37110  finxpreclem3  37851  finxpreclem5  37853  suceldisj  39281  hba1-o  39485  hlrelat2  39991  cdleme50ldil  41136  lcmineqlem23  42632  onov0suclim  43815  or3or  44563  stoweidlem14  46552  alneu  47682  2nodd  48758  elsetrecslem  50284