Theorem con3i 633

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  notnotnot  635  conax1  654  pm5.21ni  704  pm2.45  739  pm2.46  740  pm3.14  754  3ianorr  1320  nalequcoms  1531  equidqe  1546  nnal  1663  ax6blem  1664  hbnt  1667  naecoms  1738  euor2  2103  moexexdc  2129  baroco  2152  necon3ai  2416  necon3bi  2417  nnral  2487  eueq3dc  2938  difin  3401  indifdir  3420  difrab  3438  csbprc  3497  ifandc  3600  nelpri  3647  nelprd  3649  opprc  3830  opprc1  3831  opprc2  3832  notnotsnex  4221  eldifpw  4513  nlimsucg  4603  nfvres  5595  nfunsn  5596  ressnop0  5746  ovprc  5961  ovprc1  5962  ovprc2  5963  mapprc  6720  ixpprc  6787  ixp0  6799  fiprc  6883  fidceq  6939  unfiexmid  6988  difinfsnlem  7174  3nsssucpw1  7319  onntri51  7323  onntri52  7327  fzdcel  10132  bcpasc  10875  flodddiv4lt  12120  bj-nnan  15466  bj-imnimnn  15468  nnnotnotr  15720  nninfsellemsuc  15743