Theorem con2i 139

Description: A contraposition inference. Its associated inference is mt2 199. (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  193  pm3.14  993  pclem6  1023  hba1w  2051  axc4  2316  festinoALT  2677  necon3aiOLD  2970  necon2ai  2974  necon2bi  2975  eueq3  3647  ssnpss  4039  psstr  4040  elndif  4064  n0i  4268  axnulALT  5229  nfcvb  5300  zfpair  5345  epelg  5497  onxpdisj  6390  ftpg  7037  nlimsucg  7698  reldmtpos  8059  bren2  8780  sdom0OLD  8905  domunsn  8923  sdom1  9031  enp1i  9061  alephval3  9875  cdainflem  9952  ackbij1lem18  10002  isfin4p1  10080  fincssdom  10088  fin23lem41  10117  fin17  10159  fin1a2lem7  10171  axcclem  10222  pwcfsdom  10348  canthp1lem1  10417  hargch  10438  winainflem  10458  ltxrlt  11054  xmullem2  13008  rexmul  13014  xlemul1a  13031  fzdisj  13292  lcmfunsnlem2lem2  16353  smndex1n0mnd  18560  pmtrdifellem4  19096  psgnunilem3  19113  frgpcyg  20790  dvlog2lem  25816  lgsval2lem  26464  strlem1  30621  chrelat2i  30736  dfrdg4  34262  finminlem  34516  bj-nimn  34753  bj-modald  34863  finxpreclem3  35573  finxpreclem5  35575  hba1-o  36918  hlrelat2  37424  cdleme50ldil  38569  lcmineqlem23  40066  sn-dtru  40195  or3or  41638  stoweidlem14  43562  alneu  44627  2nodd  45377  elsetrecslem  46415