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  4522  nlimsucg  4612  nfvres  5604  nfunsn  5605  ressnop0  5755  ovprc  5970  ovprc1  5971  ovprc2  5972  mapprc  6729  ixpprc  6796  ixp0  6808  fiprc  6892  fidceq  6948  unfiexmid  6997  difinfsnlem  7183  3nsssucpw1  7330  onntri51  7334  onntri52  7338  fzdcel  10144  bcpasc  10892  flodddiv4lt  12168  bj-nnan  15536  bj-imnimnn  15538  nnnotnotr  15790  nninfsellemsuc  15813