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  710  pm2.45  745  pm2.46  746  pm3.14  760  3ianorr  1345  nalequcoms  1565  equidqe  1580  nnal  1697  ax6blem  1698  hbnt  1701  naecoms  1772  euor2  2138  moexexdc  2164  baroco  2187  necon3ai  2451  necon3bi  2452  nnral  2522  eueq3dc  2980  difin  3444  indifdir  3463  difrab  3481  csbprc  3540  ifandc  3646  nelpri  3693  nelprd  3695  opprc  3883  opprc1  3884  opprc2  3885  notnotsnex  4277  eldifpw  4574  nlimsucg  4664  nfvres  5675  nfunsn  5676  ressnop0  5835  ovprc  6054  ovprc1  6055  ovprc2  6056  mapprc  6821  ixpprc  6888  ixp0  6900  fiprc  6990  fidceq  7056  elssdc  7094  unfiexmid  7110  difinfsnlem  7298  3nsssucpw1  7454  onntri51  7458  onntri52  7462  fzdcel  10275  bcpasc  11029  pfxclz  11264  flodddiv4lt  12504  bj-nnan  16358  bj-imnimnn  16360  nnnotnotr  16611  nninfsellemsuc  16640