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  2176  necon2ad  2458  necon2bd  2459  minel  3555  nlimsucg  4666  poirr2  5131  funun  5373  imadif  5412  infnlbti  7230  mkvprop  7362  addnidpig  7561  zltnle  9530  zdcle  9561  btwnnz  9579  prime  9584  icc0r  10166  fznlem  10281  qltnle  10509  bcval4  11020  seq3coll  11112  swrd0g  11250  fsum3cvg  11962  fsumsplit  11991  fproddccvg  12156  fprodsplitdc  12180  bitsinv1lem  12545  2sqpwodd  12771  pockthg  12953  prmunb  12958  logbgcd1irr  15720  lgsne0  15796  eupth2lem3lem4fi  16353