Theorem con3i 635

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  notnotnot  637  nsyl5  653  conax1  657  pm5.21ni  708  pm2.45  743  pm2.46  744  pm3.14  758  3ianorr  1343  nalequcoms  1563  equidqe  1578  nnal  1695  ax6blem  1696  hbnt  1699  naecoms  1770  euor2  2136  moexexdc  2162  baroco  2185  necon3ai  2449  necon3bi  2450  nnral  2520  eueq3dc  2977  difin  3441  indifdir  3460  difrab  3478  csbprc  3537  ifandc  3643  nelpri  3690  nelprd  3692  opprc  3878  opprc1  3879  opprc2  3880  notnotsnex  4271  eldifpw  4568  nlimsucg  4658  nfvres  5665  nfunsn  5666  ressnop0  5824  ovprc  6043  ovprc1  6044  ovprc2  6045  mapprc  6807  ixpprc  6874  ixp0  6886  fiprc  6976  fidceq  7039  elssdc  7075  unfiexmid  7091  difinfsnlem  7277  3nsssucpw1  7432  onntri51  7436  onntri52  7440  fzdcel  10248  bcpasc  11000  pfxclz  11226  flodddiv4lt  12464  bj-nnan  16155  bj-imnimnn  16157  nnnotnotr  16408  nninfsellemsuc  16438