Theorem con3i 627

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  notnotnot  629  conax1  648  pm5.21ni  698  pm2.45  733  pm2.46  734  pm3.14  748  3ianorr  1304  nalequcoms  1510  equidqe  1525  nnal  1642  ax6blem  1643  hbnt  1646  naecoms  1717  euor2  2077  moexexdc  2103  baroco  2126  necon3ai  2389  necon3bi  2390  nnral  2460  eueq3dc  2904  difin  3364  indifdir  3383  difrab  3401  csbprc  3460  ifandc  3563  nelpri  3607  nelprd  3609  opprc  3786  opprc1  3787  opprc2  3788  notnotsnex  4173  eldifpw  4462  nlimsucg  4550  nfvres  5529  nfunsn  5530  ressnop0  5677  ovprc  5888  ovprc1  5889  ovprc2  5890  mapprc  6630  ixpprc  6697  ixp0  6709  fiprc  6793  fidceq  6847  unfiexmid  6895  difinfsnlem  7076  3nsssucpw1  7213  onntri51  7217  onntri52  7221  fzdcel  9996  bcpasc  10700  flodddiv4lt  11895  bj-nnan  13771  bj-imnimnn  13773  nnnotnotr  14025  nninfsellemsuc  14045