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  998  pclem6  1028  hba1w  2047  axc4  2321  festinoALT  2675  necon3aiOLD  2966  necon2ai  2970  necon2bi  2971  eueq3  3717  ssnpss  4106  psstr  4107  elndif  4133  n0i  4340  axnulALT  5304  nfcvb  5376  zfpair  5421  epelg  5585  onxpdisj  6510  ftpg  7176  nlimsucg  7863  reldmtpos  8259  bren2  9023  sdom0OLD  9149  domunsn  9167  sdom1OLD  9279  1sdom2dom  9283  enp1iOLD  9314  alephval3  10150  cdainflem  10228  ackbij1lem18  10276  isfin4p1  10355  fincssdom  10363  fin23lem41  10392  fin17  10434  fin1a2lem7  10446  axcclem  10497  pwcfsdom  10623  canthp1lem1  10692  hargch  10713  winainflem  10733  ltxrlt  11331  xmullem2  13307  rexmul  13313  xlemul1a  13330  fzdisj  13591  lcmfunsnlem2lem2  16676  smndex1n0mnd  18925  pmtrdifellem4  19497  psgnunilem3  19514  frgpcyg  21592  dvlog2lem  26694  lgsval2lem  27351  elons2  28281  strlem1  32269  chrelat2i  32384  dfrdg4  35952  finminlem  36319  bj-nimn  36564  bj-modald  36674  finxpreclem3  37394  finxpreclem5  37396  hba1-o  38898  hlrelat2  39405  cdleme50ldil  40550  lcmineqlem23  42052  onov0suclim  43287  or3or  44036  stoweidlem14  46029  alneu  47136  2nodd  48088  elsetrecslem  49218