Theorem con2i 137

Description: A contraposition inference. Its associated inference is mt2 192. (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 136	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  138  notnot  139  pm2.65i  186  pm3.14  1023  pclem6  1054  hba1w  2149  axc4  2352  festinoALT  2760  calemesOLD  2777  fresisonOLD  2781  calemosOLD  2783  fesapoOLD  2785  necon3ai  3024  necon2ai  3028  necon2bi  3029  eueq3  3606  ssnpss  3938  psstr  3939  elndif  3963  n0i  4151  axnulALT  5013  nfcvb  5078  zfpair  5127  onxpdisj  6086  ftpg  6679  nlimsucg  7308  reldmtpos  7630  bren2  8259  sdom0  8367  domunsn  8385  sdom1  8435  enp1i  8470  alephval3  9253  dfac2OLD  9275  cdainflem  9335  ackbij1lem18  9381  isfin4-3  9459  fincssdom  9467  fin23lem41  9496  fin45  9536  fin17  9538  fin1a2lem7  9550  axcclem  9601  pwcfsdom  9727  canthp1lem1  9796  hargch  9817  winainflem  9837  ltxrlt  10434  xmullem2  12390  rexmul  12396  xlemul1a  12413  fzdisj  12668  lcmfunsnlem2lem2  15732  pmtrdifellem4  18256  psgnunilem3  18274  frgpcyg  20288  dvlog2lem  24804  lgsval2lem  25452  strlem1  29660  chrelat2i  29775  dfrdg4  32592  finminlem  32846  bj-nimn  33074  bj-modald  33195  finxpreclem3  33774  finxpreclem5  33776  hba1-o  34971  hlrelat2  35477  cdleme50ldil  36622  or3or  39158  stoweidlem14  41023  alneu  42024  2nodd  42677  elsetrecslem  43354