Theorem con2i 134

Description: A contraposition inference. Its associated inference is mt2 191. (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 133	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  135  notnot  136  pm2.65i  185  pm3.14  522  pclem6  991  hba1w  2016  hba1wOLD  2017  axc4  2168  festino  2600  calemes  2610  fresison  2612  calemos  2613  fesapo  2614  necon3ai  2848  necon2ai  2852  necon2bi  2853  eueq3  3414  ssnpss  3743  psstr  3744  elndif  3767  n0i  3953  axnulALT  4820  nfcvb  4928  zfpair  4934  onxpdisj  5885  funtpgOLD  5981  ftpg  6463  nlimsucg  7084  reldmtpos  7405  bren2  8028  sdom0  8133  domunsn  8151  sdom1  8201  enp1i  8236  alephval3  8971  dfac2  8991  cdainflem  9051  ackbij1lem18  9097  isfin4-3  9175  fincssdom  9183  fin23lem41  9212  fin45  9252  fin17  9254  fin1a2lem7  9266  axcclem  9317  pwcfsdom  9443  canthp1lem1  9512  hargch  9533  winainflem  9553  ltxrlt  10146  xmullem2  12133  rexmul  12139  xlemul1a  12156  fzdisj  12406  lcmfunsnlem2lem2  15399  pmtrdifellem4  17945  psgnunilem3  17962  frgpcyg  19970  dvlog2lem  24443  lgsval2lem  25077  strlem1  29237  chrelat2i  29352  dfrdg4  32183  finminlem  32437  bj-nimn  32676  bj-modald  32786  finxpreclem3  33360  finxpreclem5  33362  hba1-o  34501  hlrelat2  35007  cdleme50ldil  36153  or3or  38636  stoweidlem14  40549  alneu  41522  2nodd  42137  elsetrecslem  42770