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  2081  axc4  2351  festinoALT  2699  necon2ai  2984  necon2bi  2985  eueq3  3668  ssnpss  4034  psstr  4035  elndif  4069  n0i  4285  axnulALT  5257  nfcvb  5337  zfpair  5382  epelg  5551  onxpdisj  6490  ftpg  7160  nlimsucg  7853  reldmtpos  8254  bren2  9013  domunsn  9149  1sdom2dom  9248  nelaneqOLD  9600  alephval3  10192  cdainflem  10269  ackbij1lem18  10317  isfin4p1  10396  fincssdom  10404  fin23lem41  10433  fin17  10475  fin1a2lem7  10487  axcclem  10538  pwcfsdom  10671  canthp1lem1  10740  hargch  10761  winainflem  10781  ltxrlt  11383  xmullem2  13398  rexmul  13404  xlemul1a  13421  fzdisj  13688  lcmfunsnlem2lem2  16819  smndex1n0mnd  19116  pmtrdifellem4  19698  psgnunilem3  19715  frgpcyg  21884  dvlog2lem  26985  lgsval2lem  27639  elons2  28649  oldfib  28768  strlem1  32857  chrelat2i  32972  xoromon  35767  onvf1odlem1  35950  dfrdg4  36807  finminlem  37198  regsfromsetind  37419  regsfromunir1  37420  bj-nimn  37524  bj-modald  37665  finxpreclem3  38409  finxpreclem5  38411  suceldisj  39843  hba1-o  40047  hlrelat2  40553  cdleme50ldil  41698  lcmineqlem23  43194  onov0suclim  44369  or3or  45116  stoweidlem14  47117  alneu  48287  2nodd  49362  elsetrecslem  50960