Theorem con2d 613

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

This theorem is referenced by:  mt2d  614  con3d  620  pm3.2im  626  con2  632  pm2.65  648  con1biimdc  858  exists2  2096  necon2ad  2365  necon2bd  2366  minel  3424  nlimsucg  4481  poirr2  4931  funun  5167  imadif  5203  infnlbti  6913  mkvprop  7032  addnidpig  7144  zltnle  9100  zdcle  9127  btwnnz  9145  prime  9150  icc0r  9709  fznlem  9821  qltnle  10023  bcval4  10498  seq3coll  10585  fsum3cvg  11147  fsumsplit  11176  fproddccvg  11341  2sqpwodd  11854