Theorem con2d 625

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 616	. . . 4 ⊢ (¬ 𝜒 → (𝜒 → ¬ 𝜓))
3	1, 2	syl6 33	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → ¬ 𝜓)))
4	3	com23 78	. 2 ⊢ (𝜑 → (𝜒 → (𝜓 → ¬ 𝜓)))
5		pm2.01 617	. 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 615  ax-in2 616

This theorem is referenced by:  mt2d  626  con3d  632  pm3.2im  638  con2  644  pm2.65  660  con1biimdc  874  exists2  2142  necon2ad  2424  necon2bd  2425  minel  3513  nlimsucg  4603  poirr2  5063  funun  5303  imadif  5339  infnlbti  7101  mkvprop  7233  addnidpig  7422  zltnle  9391  zdcle  9421  btwnnz  9439  prime  9444  icc0r  10020  fznlem  10135  qltnle  10352  bcval4  10863  seq3coll  10953  fsum3cvg  11562  fsumsplit  11591  fproddccvg  11756  fprodsplitdc  11780  bitsinv1lem  12145  2sqpwodd  12371  pockthg  12553  prmunb  12558  logbgcd1irr  15289  lgsne0  15365