Theorem con3i 641

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 637	1 ⊢ (¬ 𝜓 → ¬ 𝜑)

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  notnotnot  643  nsyl5  659  conax1  663  pm5.21ni  715  pm2.45  750  pm2.46  751  pm3.14  765  3ianorr  1350  nalequcoms  1570  equidqe  1585  nnal  1702  hbn  1703  hbnt  1705  naecoms  1776  euor2  2145  moexexdc  2171  baroco  2194  necon3ai  2469  necon3bi  2470  nnral  2540  eueq3dc  3000  difin  3468  indifdir  3487  difrab  3507  csbprc  3571  ifandc  3678  nelpri  3729  nelprd  3731  opprc  3920  opprc1  3921  opprc2  3922  notnotsnex  4319  eldifpw  4618  nlimsucg  4708  nfvres  5726  nfunsn  5727  ressnop0  5887  ovprc  6111  ovprc1  6112  ovprc2  6113  mapprc  6916  fsetdmprc0  6940  ixpprc  6991  ixp0  7003  fiprc  7094  fidceq  7161  elssdc  7199  unfiexmid  7215  relprcnfsupp  7278  difinfsnlem  7429  3nsssucpw1  7585  onntri51  7589  onntri52  7593  fzdcel  10423  bcpasc  11182  hashfibc  11261  hashf1lem2  11264  pfxclz  11429  flodddiv4lt  12683  bj-nnan  16678  bj-imnimnn  16680  nnnotnotr  16930  nninfsellemsuc  16960