Theorem con2i 126

Description: A contraposition inference. Its associated inference is mt2 186. (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 125	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  127  notnot  128  pm2.65i  180  pm3.14  516  pclem6  957  hba1w  1922  axc4  1991  festino  2454  calemes  2464  fresison  2466  calemos  2467  fesapo  2468  necon3ai  2702  necon2ai  2706  necon2bi  2707  eueq3  3237  ssnpss  3558  psstr  3559  elndif  3582  n0i  3762  axnulALT  4564  nfcvb  4671  zfpair  4678  onssneli  5583  onxpdisj  5593  funtpg  5684  ftpg  6142  nlimsucg  6746  reldmtpos  7058  bren2  7683  sdom0  7788  domunsn  7806  sdom1  7856  enp1i  7891  alephval3  8626  dfac2  8646  cdainflem  8706  ackbij1lem18  8752  isfin4-3  8830  fincssdom  8838  fin23lem41  8867  fin45  8907  fin17  8909  fin1a2lem7  8921  axcclem  8972  pwcfsdom  9093  canthp1lem1  9162  hargch  9183  winainflem  9203  ltxrlt  9789  xmullem2  11646  rexmul  11652  xlemul1a  11669  fzdisj  11922  lcmfunsnlem2lem2  14774  pmtrdifellem4  17281  psgnunilem3  17298  frgpcyg  19302  dvlog2lem  23758  lgsval2lem  24395  isusgra0  25235  usgraop  25238  cusgrares  25361  2pthlem2  25487  2spot0  25952  strlem1  28066  chrelat2i  28181  dfrdg4  30869  finminlem  31123  bj-nimn  31331  bj-modald  31454  finxpreclem3  32006  finxpreclem5  32008  hba1-o  32702  hlrelat2  33208  cdleme50ldil  34355  stoweidlem14  38310  alneu  39142  2nodd  41002