Theorem con2d 629

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

This theorem is referenced by:  mt2d  630  con3d  636  pm3.2im  642  con2  648  pm2.65  665  con1biimdc  880  exists2  2177  necon2ad  2459  necon2bd  2460  minel  3556  nlimsucg  4664  poirr2  5129  funun  5371  imadif  5410  infnlbti  7225  mkvprop  7357  addnidpig  7556  zltnle  9525  zdcle  9556  btwnnz  9574  prime  9579  icc0r  10161  fznlem  10276  qltnle  10504  bcval4  11015  seq3coll  11107  swrd0g  11242  fsum3cvg  11941  fsumsplit  11970  fproddccvg  12135  fprodsplitdc  12159  bitsinv1lem  12524  2sqpwodd  12750  pockthg  12932  prmunb  12937  logbgcd1irr  15694  lgsne0  15770  eupth2lem3lem4fi  16327