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  5834  ovprc  6053  ovprc1  6054  ovprc2  6055  mapprc  6820  ixpprc  6887  ixp0  6899  fiprc  6989  fidceq  7055  elssdc  7093  unfiexmid  7109  difinfsnlem  7297  3nsssucpw1  7453  onntri51  7457  onntri52  7461  fzdcel  10274  bcpasc  11027  pfxclz  11259  flodddiv4lt  12498  bj-nnan  16332  bj-imnimnn  16334  nnnotnotr  16585  nninfsellemsuc  16614