Theorem con2i 141

Description: A contraposition inference. Its associated inference is mt2 202. (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 140	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  142  notnot  144  pm2.65i  196  pm3.14  992  pclem6  1022  hba1w  2054  axc4  2340  festinoALT  2760  necon3ai  3041  necon2ai  3045  necon2bi  3046  eueq3  3702  ssnpss  4080  psstr  4081  elndif  4105  n0i  4299  axnulALT  5208  nfcvb  5277  zfpair  5322  epelg  5466  onxpdisj  6310  ftpg  6918  nlimsucg  7557  reldmtpos  7900  bren2  8540  sdom0  8649  domunsn  8667  sdom1  8718  enp1i  8753  alephval3  9536  cdainflem  9613  ackbij1lem18  9659  isfin4p1  9737  fincssdom  9745  fin23lem41  9774  fin17  9816  fin1a2lem7  9828  axcclem  9879  pwcfsdom  10005  canthp1lem1  10074  hargch  10095  winainflem  10115  ltxrlt  10711  xmullem2  12659  rexmul  12665  xlemul1a  12682  fzdisj  12935  lcmfunsnlem2lem2  15983  smndex1n0mnd  18077  pmtrdifellem4  18607  psgnunilem3  18624  frgpcyg  20720  dvlog2lem  25235  lgsval2lem  25883  strlem1  30027  chrelat2i  30142  dfrdg4  33412  finminlem  33666  bj-nimn  33899  bj-modald  34006  finxpreclem3  34677  finxpreclem5  34679  hba1-o  36048  hlrelat2  36554  cdleme50ldil  37699  sn-dtru  39131  or3or  40391  stoweidlem14  42319  alneu  43343  2nodd  44099  elsetrecslem  44821