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  2978  difin  3442  indifdir  3461  difrab  3479  csbprc  3538  ifandc  3644  nelpri  3691  nelprd  3693  opprc  3881  opprc1  3882  opprc2  3883  notnotsnex  4275  eldifpw  4572  nlimsucg  4662  nfvres  5671  nfunsn  5672  ressnop0  5830  ovprc  6049  ovprc1  6050  ovprc2  6051  mapprc  6816  ixpprc  6883  ixp0  6895  fiprc  6985  fidceq  7051  elssdc  7087  unfiexmid  7103  difinfsnlem  7289  3nsssucpw1  7444  onntri51  7448  onntri52  7452  fzdcel  10265  bcpasc  11018  pfxclz  11250  flodddiv4lt  12489  bj-nnan  16268  bj-imnimnn  16270  nnnotnotr  16521  nninfsellemsuc  16550