Theorem con2d 627

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

This theorem is referenced by:  mt2d  628  con3d  634  pm3.2im  640  con2  646  pm2.65  663  con1biimdc  878  exists2  2175  necon2ad  2457  necon2bd  2458  minel  3553  nlimsucg  4659  poirr2  5124  funun  5365  imadif  5404  infnlbti  7209  mkvprop  7341  addnidpig  7539  zltnle  9508  zdcle  9539  btwnnz  9557  prime  9562  icc0r  10139  fznlem  10254  qltnle  10480  bcval4  10991  seq3coll  11082  swrd0g  11213  fsum3cvg  11910  fsumsplit  11939  fproddccvg  12104  fprodsplitdc  12128  bitsinv1lem  12493  2sqpwodd  12719  pockthg  12901  prmunb  12906  logbgcd1irr  15662  lgsne0  15738