Theorem con3i 637

Description: A contraposition inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 20-Jun-2013.)

Hypothesis

Ref	Expression
con3i.a	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
con3i	⊢ (¬ 𝜓 → ¬ 𝜑)

Proof of Theorem con3i

Step	Hyp	Ref	Expression
1		id 19	. 2 ⊢ (¬ 𝜓 → ¬ 𝜓)
2		con3i.a	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	nsyl 633	1 ⊢ (¬ 𝜓 → ¬ 𝜑)

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 619  ax-in2 620

This theorem is referenced by:  notnotnot  639  nsyl5  655  conax1  659  pm5.21ni  711  pm2.45  746  pm2.46  747  pm3.14  761  3ianorr  1346  nalequcoms  1566  equidqe  1581  nnal  1698  hbn  1699  hbnt  1701  naecoms  1772  euor2  2141  moexexdc  2167  baroco  2190  necon3ai  2463  necon3bi  2464  nnral  2534  eueq3dc  2994  difin  3462  indifdir  3481  difrab  3499  csbprc  3558  ifandc  3667  nelpri  3718  nelprd  3720  opprc  3909  opprc1  3910  opprc2  3911  notnotsnex  4305  eldifpw  4603  nlimsucg  4693  nfvres  5711  nfunsn  5712  ressnop0  5870  ovprc  6094  ovprc1  6095  ovprc2  6096  mapprc  6899  ixpprc  6967  ixp0  6979  fiprc  7070  fidceq  7137  elssdc  7175  unfiexmid  7191  relprcnfsupp  7254  difinfsnlem  7403  3nsssucpw1  7559  onntri51  7563  onntri52  7567  fzdcel  10394  bcpasc  11153  hashfibc  11232  pfxclz  11396  flodddiv4lt  12649  bj-nnan  16634  bj-imnimnn  16636  nnnotnotr  16886  nninfsellemsuc  16916