Theorem con2i 139

Description: A contraposition inference. Its associated inference is mt2 200. (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  194  pm3.14  998  pclem6  1028  hba1w  2051  axc4  2327  festinoALT  2676  necon2ai  2962  necon2bi  2963  eueq3  3658  ssnpss  4047  psstr  4048  elndif  4074  n0i  4281  axnulALT  5239  nfcvb  5313  zfpair  5358  epelg  5525  onxpdisj  6444  ftpg  7103  nlimsucg  7786  reldmtpos  8177  bren2  8923  domunsn  9058  1sdom2dom  9157  nelaneq  9509  alephval3  10023  cdainflem  10101  ackbij1lem18  10149  isfin4p1  10228  fincssdom  10236  fin23lem41  10265  fin17  10307  fin1a2lem7  10319  axcclem  10370  pwcfsdom  10497  canthp1lem1  10566  hargch  10587  winainflem  10607  ltxrlt  11207  xmullem2  13208  rexmul  13214  xlemul1a  13231  fzdisj  13496  lcmfunsnlem2lem2  16599  smndex1n0mnd  18874  pmtrdifellem4  19445  psgnunilem3  19462  frgpcyg  21563  dvlog2lem  26629  lgsval2lem  27284  elons2  28264  oldfib  28383  strlem1  32336  chrelat2i  32451  xoromon  35248  onvf1odlem1  35301  dfrdg4  36149  finminlem  36516  regsfromsetind  36737  regsfromunir1  36738  bj-nimn  36843  bj-modald  36984  finxpreclem3  37723  finxpreclem5  37725  suceldisj  39153  hba1-o  39357  hlrelat2  39863  cdleme50ldil  41008  lcmineqlem23  42504  onov0suclim  43720  or3or  44468  stoweidlem14  46460  alneu  47584  2nodd  48660  elsetrecslem  50186