Theorem con2i 139

Description: A contraposition inference. Its associated inference is mt2 201. (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  195  pm3.14  1003  pclem6  1033  hba1w  2056  axc4  2330  festinoALT  2679  necon2ai  2964  necon2bi  2965  eueq3  3659  ssnpss  4044  psstr  4045  elndif  4070  n0i  4275  axnulALT  5233  nfcvb  5312  zfpair  5357  epelg  5526  onxpdisj  6444  ftpg  7106  nlimsucg  7789  reldmtpos  8181  bren2  8927  domunsn  9062  1sdom2dom  9161  nelaneqOLD  9515  alephval3  10030  cdainflem  10108  ackbij1lem18  10156  isfin4p1  10235  fincssdom  10243  fin23lem41  10272  fin17  10314  fin1a2lem7  10326  axcclem  10377  pwcfsdom  10504  canthp1lem1  10573  hargch  10594  winainflem  10614  ltxrlt  11214  xmullem2  13215  rexmul  13221  xlemul1a  13238  fzdisj  13503  lcmfunsnlem2lem2  16606  smndex1n0mnd  18881  pmtrdifellem4  19452  psgnunilem3  19469  frgpcyg  21555  dvlog2lem  26641  lgsval2lem  27295  elons2  28275  oldfib  28394  strlem1  32346  chrelat2i  32461  xoromon  35277  onvf1odlem1  35338  dfrdg4  36186  finminlem  36553  regsfromsetind  36774  regsfromunir1  36775  bj-nimn  36880  bj-modald  37021  finxpreclem3  37762  finxpreclem5  37764  suceldisj  39192  hba1-o  39396  hlrelat2  39902  cdleme50ldil  41047  lcmineqlem23  42543  onov0suclim  43726  or3or  44474  stoweidlem14  46464  alneu  47594  2nodd  48670  elsetrecslem  50196