Theorem con2i 141

Description: A contraposition inference. Its associated inference is mt2 203. (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 140	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  142  notnot  144  pm2.65i  197  pm3.14  993  pclem6  1023  hba1w  2054  axc4  2329  festinoALT  2737  necon3ai  3012  necon2ai  3016  necon2bi  3017  eueq3  3650  ssnpss  4031  psstr  4032  elndif  4056  n0i  4249  axnulALT  5172  nfcvb  5242  zfpair  5287  epelg  5431  onxpdisj  6278  ftpg  6895  nlimsucg  7537  reldmtpos  7883  bren2  8523  sdom0  8633  domunsn  8651  sdom1  8702  enp1i  8737  alephval3  9521  cdainflem  9598  ackbij1lem18  9648  isfin4p1  9726  fincssdom  9734  fin23lem41  9763  fin17  9805  fin1a2lem7  9817  axcclem  9868  pwcfsdom  9994  canthp1lem1  10063  hargch  10084  winainflem  10104  ltxrlt  10700  xmullem2  12646  rexmul  12652  xlemul1a  12669  fzdisj  12929  lcmfunsnlem2lem2  15973  smndex1n0mnd  18069  pmtrdifellem4  18599  psgnunilem3  18616  frgpcyg  20265  dvlog2lem  25243  lgsval2lem  25891  strlem1  30033  chrelat2i  30148  dfrdg4  33525  finminlem  33779  bj-nimn  34012  bj-modald  34119  finxpreclem3  34810  finxpreclem5  34812  hba1-o  36193  hlrelat2  36699  cdleme50ldil  37844  lcmineqlem23  39339  sn-dtru  39403  or3or  40724  stoweidlem14  42656  alneu  43680  2nodd  44432  elsetrecslem  45228