Theorem con2i 139

Description: A contraposition inference. Its associated inference is mt2 200. (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  194  pm3.14  997  pclem6  1027  hba1w  2048  axc4  2320  festinoALT  2668  necon2ai  2954  necon2bi  2955  eueq3  3682  ssnpss  4069  psstr  4070  elndif  4096  n0i  4303  axnulALT  5259  nfcvb  5331  zfpair  5376  epelg  5539  onxpdisj  6460  ftpg  7128  nlimsucg  7818  reldmtpos  8213  bren2  8954  domunsn  9091  sdom1OLD  9190  1sdom2dom  9194  enp1iOLD  9225  alephval3  10063  cdainflem  10141  ackbij1lem18  10189  isfin4p1  10268  fincssdom  10276  fin23lem41  10305  fin17  10347  fin1a2lem7  10359  axcclem  10410  pwcfsdom  10536  canthp1lem1  10605  hargch  10626  winainflem  10646  ltxrlt  11244  xmullem2  13225  rexmul  13231  xlemul1a  13248  fzdisj  13512  lcmfunsnlem2lem2  16609  smndex1n0mnd  18839  pmtrdifellem4  19409  psgnunilem3  19426  frgpcyg  21483  dvlog2lem  26561  lgsval2lem  27218  elons2  28159  strlem1  32179  chrelat2i  32294  onvf1odlem1  35090  dfrdg4  35939  finminlem  36306  bj-nimn  36551  bj-modald  36661  finxpreclem3  37381  finxpreclem5  37383  hba1-o  38890  hlrelat2  39397  cdleme50ldil  40542  lcmineqlem23  42039  onov0suclim  43263  or3or  44012  stoweidlem14  46012  alneu  47125  2nodd  48160  elsetrecslem  49688