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  2050  axc4  2324  festinoALT  2672  necon2ai  2958  necon2bi  2959  eueq3  3666  ssnpss  4055  psstr  4056  elndif  4082  n0i  4289  axnulALT  5244  nfcvb  5316  zfpair  5361  epelg  5520  onxpdisj  6438  ftpg  7095  nlimsucg  7778  reldmtpos  8170  bren2  8912  domunsn  9047  1sdom2dom  9145  nelaneq  9494  alephval3  10008  cdainflem  10086  ackbij1lem18  10134  isfin4p1  10213  fincssdom  10221  fin23lem41  10250  fin17  10292  fin1a2lem7  10304  axcclem  10355  pwcfsdom  10481  canthp1lem1  10550  hargch  10571  winainflem  10591  ltxrlt  11190  xmullem2  13166  rexmul  13172  xlemul1a  13189  fzdisj  13453  lcmfunsnlem2lem2  16552  smndex1n0mnd  18822  pmtrdifellem4  19393  psgnunilem3  19410  frgpcyg  21512  dvlog2lem  26589  lgsval2lem  27246  elons2  28196  strlem1  32232  chrelat2i  32347  onvf1odlem1  35168  dfrdg4  36016  finminlem  36383  bj-nimn  36628  bj-modald  36738  finxpreclem3  37458  finxpreclem5  37460  hba1-o  39016  hlrelat2  39522  cdleme50ldil  40667  lcmineqlem23  42164  onov0suclim  43391  or3or  44140  stoweidlem14  46136  alneu  47248  2nodd  48296  elsetrecslem  49824