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  1321  nalequcoms  1539  equidqe  1554  nnal  1671  ax6blem  1672  hbnt  1675  naecoms  1746  euor2  2111  moexexdc  2137  baroco  2160  necon3ai  2424  necon3bi  2425  nnral  2495  eueq3dc  2946  difin  3409  indifdir  3428  difrab  3446  csbprc  3505  ifandc  3609  nelpri  3656  nelprd  3658  opprc  3839  opprc1  3840  opprc2  3841  notnotsnex  4230  eldifpw  4523  nlimsucg  4613  nfvres  5609  nfunsn  5610  ressnop0  5764  ovprc  5979  ovprc1  5980  ovprc2  5981  mapprc  6738  ixpprc  6805  ixp0  6817  fiprc  6906  fidceq  6965  unfiexmid  7014  difinfsnlem  7200  3nsssucpw1  7347  onntri51  7351  onntri52  7355  fzdcel  10161  bcpasc  10909  flodddiv4lt  12191  bj-nnan  15605  bj-imnimnn  15607  nnnotnotr  15859  nninfsellemsuc  15882