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  523  pclem6  970  hba1w  1976  hba1wOLD  1977  axc4  2131  festino  2575  calemes  2585  fresison  2587  calemos  2588  fesapo  2589  necon3ai  2821  necon2ai  2825  necon2bi  2826  eueq3  3368  ssnpss  3693  psstr  3694  elndif  3717  n0i  3901  axnulALT  4752  nfcvb  4863  zfpair  4870  onxpdisj  5809  funtpgOLD  5903  ftpg  6378  nlimsucg  6990  reldmtpos  7306  bren2  7931  sdom0  8037  domunsn  8055  sdom1  8105  enp1i  8140  alephval3  8878  dfac2  8898  cdainflem  8958  ackbij1lem18  9004  isfin4-3  9082  fincssdom  9090  fin23lem41  9119  fin45  9159  fin17  9161  fin1a2lem7  9173  axcclem  9224  pwcfsdom  9350  canthp1lem1  9419  hargch  9440  winainflem  9460  ltxrlt  10053  xmullem2  12035  rexmul  12041  xlemul1a  12058  fzdisj  12307  lcmfunsnlem2lem2  15271  pmtrdifellem4  17815  psgnunilem3  17832  frgpcyg  19836  dvlog2lem  24293  lgsval2lem  24927  strlem1  28949  chrelat2i  29064  dfrdg4  31673  finminlem  31927  bj-nimn  32166  bj-modald  32276  finxpreclem3  32835  finxpreclem5  32837  hba1-o  33629  hlrelat2  34136  cdleme50ldil  35283  or3or  37768  stoweidlem14  39506  alneu  40473  2nodd  41054  elsetrecslem  41692