Theorem con2d 625

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

This theorem is referenced by:  mt2d  626  con3d  632  pm3.2im  638  con2  644  pm2.65  661  con1biimdc  875  exists2  2152  necon2ad  2434  necon2bd  2435  minel  3523  nlimsucg  4618  poirr2  5080  funun  5320  imadif  5359  infnlbti  7135  mkvprop  7267  addnidpig  7456  zltnle  9425  zdcle  9456  btwnnz  9474  prime  9479  icc0r  10055  fznlem  10170  qltnle  10393  bcval4  10904  seq3coll  10994  swrd0g  11121  fsum3cvg  11733  fsumsplit  11762  fproddccvg  11927  fprodsplitdc  11951  bitsinv1lem  12316  2sqpwodd  12542  pockthg  12724  prmunb  12729  logbgcd1irr  15483  lgsne0  15559