Theorem con2i 139

Description: A contraposition inference. Its associated inference is mt2 199. (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.65i  193  pm3.14  994  pclem6  1024  hba1w  2050  axc4  2314  festinoALT  2670  necon3aiOLD  2966  necon2ai  2970  necon2bi  2971  eueq3  3707  ssnpss  4103  psstr  4104  elndif  4128  n0i  4333  axnulALT  5304  nfcvb  5374  zfpair  5419  epelg  5581  onxpdisj  6490  ftpg  7153  nlimsucg  7830  reldmtpos  8218  bren2  8978  sdom0OLD  9108  domunsn  9126  sdom1OLD  9242  1sdom2dom  9246  enp1iOLD  9279  alephval3  10104  cdainflem  10181  ackbij1lem18  10231  isfin4p1  10309  fincssdom  10317  fin23lem41  10346  fin17  10388  fin1a2lem7  10400  axcclem  10451  pwcfsdom  10577  canthp1lem1  10646  hargch  10667  winainflem  10687  ltxrlt  11283  xmullem2  13243  rexmul  13249  xlemul1a  13266  fzdisj  13527  lcmfunsnlem2lem2  16575  smndex1n0mnd  18792  pmtrdifellem4  19346  psgnunilem3  19363  frgpcyg  21128  dvlog2lem  26159  lgsval2lem  26807  strlem1  31498  chrelat2i  31613  dfrdg4  34918  finminlem  35198  bj-nimn  35435  bj-modald  35545  finxpreclem3  36269  finxpreclem5  36271  hba1-o  37762  hlrelat2  38269  cdleme50ldil  39414  lcmineqlem23  40911  onov0suclim  42014  or3or  42764  stoweidlem14  44720  alneu  45822  2nodd  46572  elsetrecslem  47734