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  3554  nlimsucg  4662  poirr2  5127  funun  5368  imadif  5407  infnlbti  7219  mkvprop  7351  addnidpig  7549  zltnle  9518  zdcle  9549  btwnnz  9567  prime  9572  icc0r  10154  fznlem  10269  qltnle  10496  bcval4  11007  seq3coll  11099  swrd0g  11234  fsum3cvg  11932  fsumsplit  11961  fproddccvg  12126  fprodsplitdc  12150  bitsinv1lem  12515  2sqpwodd  12741  pockthg  12923  prmunb  12928  logbgcd1irr  15684  lgsne0  15760