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  3553  nlimsucg  4658  poirr2  5121  funun  5362  imadif  5401  infnlbti  7201  mkvprop  7333  addnidpig  7531  zltnle  9500  zdcle  9531  btwnnz  9549  prime  9554  icc0r  10130  fznlem  10245  qltnle  10471  bcval4  10982  seq3coll  11072  swrd0g  11200  fsum3cvg  11897  fsumsplit  11926  fproddccvg  12091  fprodsplitdc  12115  bitsinv1lem  12480  2sqpwodd  12706  pockthg  12888  prmunb  12893  logbgcd1irr  15649  lgsne0  15725