Theorem con3i 637

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  notnotnot  639  nsyl5  655  conax1  659  pm5.21ni  711  pm2.45  746  pm2.46  747  pm3.14  761  3ianorr  1346  nalequcoms  1566  equidqe  1581  nnal  1698  hbn  1699  hbnt  1701  naecoms  1772  euor2  2138  moexexdc  2164  baroco  2187  necon3ai  2452  necon3bi  2453  nnral  2523  eueq3dc  2981  difin  3446  indifdir  3465  difrab  3483  csbprc  3542  ifandc  3650  nelpri  3697  nelprd  3699  opprc  3888  opprc1  3889  opprc2  3890  notnotsnex  4283  eldifpw  4580  nlimsucg  4670  nfvres  5684  nfunsn  5685  ressnop0  5843  ovprc  6064  ovprc1  6065  ovprc2  6066  mapprc  6864  ixpprc  6931  ixp0  6943  fiprc  7033  fidceq  7099  elssdc  7137  unfiexmid  7153  difinfsnlem  7341  3nsssucpw1  7497  onntri51  7501  onntri52  7505  fzdcel  10320  bcpasc  11074  pfxclz  11309  flodddiv4lt  12562  bj-nnan  16437  bj-imnimnn  16439  nnnotnotr  16689  nninfsellemsuc  16721