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  2044  axc4  2319  festinoALT  2672  necon3aiOLD  2963  necon2ai  2967  necon2bi  2968  eueq3  3719  ssnpss  4115  psstr  4116  elndif  4142  n0i  4345  axnulALT  5309  nfcvb  5381  zfpair  5426  epelg  5589  onxpdisj  6511  ftpg  7175  nlimsucg  7862  reldmtpos  8257  bren2  9021  sdom0OLD  9147  domunsn  9165  sdom1OLD  9276  1sdom2dom  9280  enp1iOLD  9311  alephval3  10147  cdainflem  10225  ackbij1lem18  10273  isfin4p1  10352  fincssdom  10360  fin23lem41  10389  fin17  10431  fin1a2lem7  10443  axcclem  10494  pwcfsdom  10620  canthp1lem1  10689  hargch  10710  winainflem  10730  ltxrlt  11328  xmullem2  13303  rexmul  13309  xlemul1a  13326  fzdisj  13587  lcmfunsnlem2lem2  16672  smndex1n0mnd  18937  pmtrdifellem4  19511  psgnunilem3  19528  frgpcyg  21609  dvlog2lem  26708  lgsval2lem  27365  elons2  28295  strlem1  32278  chrelat2i  32393  dfrdg4  35932  finminlem  36300  bj-nimn  36545  bj-modald  36655  finxpreclem3  37375  finxpreclem5  37377  hba1-o  38878  hlrelat2  39385  cdleme50ldil  40530  lcmineqlem23  42032  onov0suclim  43263  or3or  44012  stoweidlem14  45969  alneu  47073  2nodd  48015  elsetrecslem  48929