Theorem con2d 614

Description: A contraposition deduction. (Contributed by NM, 19-Aug-1993.) (Revised by NM, 12-Feb-2013.)

Hypothesis

Ref	Expression
con2d.1	⊢ (𝜑 → (𝜓 → ¬ 𝜒))

Assertion

Ref	Expression
con2d	⊢ (𝜑 → (𝜒 → ¬ 𝜓))

Proof of Theorem con2d

Step	Hyp	Ref	Expression
1		con2d.1	. . . 4 ⊢ (𝜑 → (𝜓 → ¬ 𝜒))
2		ax-in2 605	. . . 4 ⊢ (¬ 𝜒 → (𝜒 → ¬ 𝜓))
3	1, 2	syl6 33	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → ¬ 𝜓)))
4	3	com23 78	. 2 ⊢ (𝜑 → (𝜒 → (𝜓 → ¬ 𝜓)))
5		pm2.01 606	. 2 ⊢ ((𝜓 → ¬ 𝜓) → ¬ 𝜓)
6	4, 5	syl6 33	1 ⊢ (𝜑 → (𝜒 → ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  mt2d  615  con3d  621  pm3.2im  627  con2  633  pm2.65  649  con1biimdc  859  exists2  2097  necon2ad  2366  necon2bd  2367  minel  3429  nlimsucg  4489  poirr2  4939  funun  5175  imadif  5211  infnlbti  6921  mkvprop  7040  addnidpig  7168  zltnle  9124  zdcle  9151  btwnnz  9169  prime  9174  icc0r  9739  fznlem  9852  qltnle  10054  bcval4  10530  seq3coll  10617  fsum3cvg  11179  fsumsplit  11208  fproddccvg  11373  2sqpwodd  11890  logbgcd1irr  13092