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  997  pclem6  1027  hba1w  2048  axc4  2320  festinoALT  2669  necon2ai  2955  necon2bi  2956  eueq3  3685  ssnpss  4072  psstr  4073  elndif  4099  n0i  4306  axnulALT  5262  nfcvb  5334  zfpair  5379  epelg  5542  onxpdisj  6463  ftpg  7131  nlimsucg  7821  reldmtpos  8216  bren2  8957  domunsn  9097  sdom1OLD  9197  1sdom2dom  9201  enp1iOLD  9232  alephval3  10070  cdainflem  10148  ackbij1lem18  10196  isfin4p1  10275  fincssdom  10283  fin23lem41  10312  fin17  10354  fin1a2lem7  10366  axcclem  10417  pwcfsdom  10543  canthp1lem1  10612  hargch  10633  winainflem  10653  ltxrlt  11251  xmullem2  13232  rexmul  13238  xlemul1a  13255  fzdisj  13519  lcmfunsnlem2lem2  16616  smndex1n0mnd  18846  pmtrdifellem4  19416  psgnunilem3  19433  frgpcyg  21490  dvlog2lem  26568  lgsval2lem  27225  elons2  28166  strlem1  32186  chrelat2i  32301  onvf1odlem1  35097  dfrdg4  35946  finminlem  36313  bj-nimn  36558  bj-modald  36668  finxpreclem3  37388  finxpreclem5  37390  hba1-o  38897  hlrelat2  39404  cdleme50ldil  40549  lcmineqlem23  42046  onov0suclim  43270  or3or  44019  stoweidlem14  46019  alneu  47129  2nodd  48164  elsetrecslem  49692