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  2103  necon2ad  2384  necon2bd  2385  minel  3455  nlimsucg  4523  poirr2  4975  funun  5211  imadif  5247  infnlbti  6962  mkvprop  7084  addnidpig  7239  zltnle  9196  zdcle  9223  btwnnz  9241  prime  9246  icc0r  9812  fznlem  9925  qltnle  10127  bcval4  10608  seq3coll  10695  fsum3cvg  11257  fsumsplit  11286  fproddccvg  11451  fprodsplitdc  11475  2sqpwodd  12030  logbgcd1irr  13244