Theorem con2i 139

Description: A contraposition inference. Its associated inference is mt2 199. (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  193  pm3.14  992  pclem6  1022  hba1w  2048  axc4  2312  festinoALT  2668  necon3aiOLD  2964  necon2ai  2968  necon2bi  2969  eueq3  3708  ssnpss  4104  psstr  4105  elndif  4129  n0i  4334  axnulALT  5305  nfcvb  5375  zfpair  5420  epelg  5582  onxpdisj  6491  ftpg  7157  nlimsucg  7835  reldmtpos  8223  bren2  8983  sdom0OLD  9113  domunsn  9131  sdom1OLD  9247  1sdom2dom  9251  enp1iOLD  9284  alephval3  10109  cdainflem  10186  ackbij1lem18  10236  isfin4p1  10314  fincssdom  10322  fin23lem41  10351  fin17  10393  fin1a2lem7  10405  axcclem  10456  pwcfsdom  10582  canthp1lem1  10651  hargch  10672  winainflem  10692  ltxrlt  11290  xmullem2  13250  rexmul  13256  xlemul1a  13273  fzdisj  13534  lcmfunsnlem2lem2  16582  smndex1n0mnd  18831  pmtrdifellem4  19390  psgnunilem3  19407  frgpcyg  21350  dvlog2lem  26394  lgsval2lem  27044  elons2  27922  strlem1  31768  chrelat2i  31883  dfrdg4  35225  finminlem  35508  bj-nimn  35745  bj-modald  35855  finxpreclem3  36579  finxpreclem5  36581  hba1-o  38072  hlrelat2  38579  cdleme50ldil  39724  lcmineqlem23  41224  onov0suclim  42328  or3or  43078  stoweidlem14  45030  alneu  46132  2nodd  46850  elsetrecslem  47833