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  2139  moexexdc  2165  baroco  2188  necon3ai  2461  necon3bi  2462  nnral  2532  eueq3dc  2991  difin  3458  indifdir  3477  difrab  3495  csbprc  3554  ifandc  3663  nelpri  3713  nelprd  3715  opprc  3904  opprc1  3905  opprc2  3906  notnotsnex  4300  eldifpw  4598  nlimsucg  4688  nfvres  5706  nfunsn  5707  ressnop0  5865  ovprc  6086  ovprc1  6087  ovprc2  6088  mapprc  6886  ixpprc  6954  ixp0  6966  fiprc  7057  fidceq  7124  elssdc  7162  unfiexmid  7178  relprcnfsupp  7241  difinfsnlem  7390  3nsssucpw1  7546  onntri51  7550  onntri52  7554  fzdcel  10374  bcpasc  11128  hashfibc  11207  pfxclz  11371  flodddiv4lt  12624  bj-nnan  16508  bj-imnimnn  16510  nnnotnotr  16760  nninfsellemsuc  16790