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  3400  indifdir  3419  difrab  3437  csbprc  3496  ifandc  3599  nelpri  3646  nelprd  3648  opprc  3829  opprc1  3830  opprc2  3831  notnotsnex  4220  eldifpw  4512  nlimsucg  4602  nfvres  5592  nfunsn  5593  ressnop0  5743  ovprc  5957  ovprc1  5958  ovprc2  5959  mapprc  6711  ixpprc  6778  ixp0  6790  fiprc  6874  fidceq  6930  unfiexmid  6979  difinfsnlem  7165  3nsssucpw1  7303  onntri51  7307  onntri52  7311  fzdcel  10115  bcpasc  10858  flodddiv4lt  12103  bj-nnan  15382  bj-imnimnn  15384  nnnotnotr  15636  nninfsellemsuc  15656