Theorem con3i 632

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  notnotnot  634  conax1  653  pm5.21ni  703  pm2.45  738  pm2.46  739  pm3.14  753  3ianorr  1309  nalequcoms  1517  equidqe  1532  nnal  1649  ax6blem  1650  hbnt  1653  naecoms  1724  euor2  2084  moexexdc  2110  baroco  2133  necon3ai  2396  necon3bi  2397  nnral  2467  eueq3dc  2912  difin  3373  indifdir  3392  difrab  3410  csbprc  3469  ifandc  3573  nelpri  3617  nelprd  3619  opprc  3800  opprc1  3801  opprc2  3802  notnotsnex  4188  eldifpw  4478  nlimsucg  4566  nfvres  5549  nfunsn  5550  ressnop0  5698  ovprc  5910  ovprc1  5911  ovprc2  5912  mapprc  6652  ixpprc  6719  ixp0  6731  fiprc  6815  fidceq  6869  unfiexmid  6917  difinfsnlem  7098  3nsssucpw1  7235  onntri51  7239  onntri52  7243  fzdcel  10040  bcpasc  10746  flodddiv4lt  11941  bj-nnan  14491  bj-imnimnn  14493  nnnotnotr  14745  nninfsellemsuc  14764