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  3673  ssnpss  4059  psstr  4060  elndif  4086  n0i  4293  axnulALT  5246  nfcvb  5318  zfpair  5363  epelg  5524  onxpdisj  6438  ftpg  7094  nlimsucg  7782  reldmtpos  8174  bren2  8915  domunsn  9051  1sdom2dom  9153  enp1iOLD  9183  nelaneq  9512  alephval3  10023  cdainflem  10101  ackbij1lem18  10149  isfin4p1  10228  fincssdom  10236  fin23lem41  10265  fin17  10307  fin1a2lem7  10319  axcclem  10370  pwcfsdom  10496  canthp1lem1  10565  hargch  10586  winainflem  10606  ltxrlt  11204  xmullem2  13185  rexmul  13191  xlemul1a  13208  fzdisj  13472  lcmfunsnlem2lem2  16568  smndex1n0mnd  18804  pmtrdifellem4  19376  psgnunilem3  19393  frgpcyg  21498  dvlog2lem  26577  lgsval2lem  27234  elons2  28182  strlem1  32212  chrelat2i  32327  onvf1odlem1  35075  dfrdg4  35924  finminlem  36291  bj-nimn  36536  bj-modald  36646  finxpreclem3  37366  finxpreclem5  37368  hba1-o  38875  hlrelat2  39382  cdleme50ldil  40527  lcmineqlem23  42024  onov0suclim  43247  or3or  43996  stoweidlem14  45996  alneu  47109  2nodd  48157  elsetrecslem  49685