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  3877  opprc1  3878  opprc2  3879  notnotsnex  4270  eldifpw  4567  nlimsucg  4657  nfvres  5662  nfunsn  5663  ressnop0  5819  ovprc  6036  ovprc1  6037  ovprc2  6038  mapprc  6797  ixpprc  6864  ixp0  6876  fiprc  6966  fidceq  7027  unfiexmid  7076  difinfsnlem  7262  3nsssucpw1  7417  onntri51  7421  onntri52  7425  fzdcel  10232  bcpasc  10983  pfxclz  11206  flodddiv4lt  12444  bj-nnan  16058  bj-imnimnn  16060  nnnotnotr  16311  nninfsellemsuc  16337