Theorem con2d 624

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

This theorem is referenced by:  mt2d  625  con3d  631  pm3.2im  637  con2  643  pm2.65  659  con1biimdc  873  exists2  2123  necon2ad  2404  necon2bd  2405  minel  3484  nlimsucg  4563  poirr2  5018  funun  5257  imadif  5293  infnlbti  7020  mkvprop  7151  addnidpig  7330  zltnle  9293  zdcle  9323  btwnnz  9341  prime  9346  icc0r  9920  fznlem  10034  qltnle  10239  bcval4  10723  seq3coll  10813  fsum3cvg  11377  fsumsplit  11406  fproddccvg  11571  fprodsplitdc  11595  2sqpwodd  12166  pockthg  12345  prmunb  12350  logbgcd1irr  14167  lgsne0  14221