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  2051  axc4  2319  festinoALT  2676  necon3aiOLD  2968  necon2ai  2972  necon2bi  2973  eueq3  3641  ssnpss  4034  psstr  4035  elndif  4059  n0i  4264  axnulALT  5223  nfcvb  5294  zfpair  5339  epelg  5487  onxpdisj  6371  ftpg  7010  nlimsucg  7664  reldmtpos  8021  bren2  8726  sdom0  8845  domunsn  8863  sdom1  8952  enp1i  8982  alephval3  9797  cdainflem  9874  ackbij1lem18  9924  isfin4p1  10002  fincssdom  10010  fin23lem41  10039  fin17  10081  fin1a2lem7  10093  axcclem  10144  pwcfsdom  10270  canthp1lem1  10339  hargch  10360  winainflem  10380  ltxrlt  10976  xmullem2  12928  rexmul  12934  xlemul1a  12951  fzdisj  13212  lcmfunsnlem2lem2  16272  smndex1n0mnd  18466  pmtrdifellem4  19002  psgnunilem3  19019  frgpcyg  20693  dvlog2lem  25712  lgsval2lem  26360  strlem1  30513  chrelat2i  30628  dfrdg4  34180  finminlem  34434  bj-nimn  34671  bj-modald  34781  finxpreclem3  35491  finxpreclem5  35493  hba1-o  36838  hlrelat2  37344  cdleme50ldil  38489  lcmineqlem23  39987  sn-dtru  40116  or3or  41520  stoweidlem14  43445  alneu  44503  2nodd  45254  elsetrecslem  46290