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  881  exists2  2178  necon2ad  2469  necon2bd  2470  minel  3569  nlimsucg  4687  poirr2  5154  funun  5396  imadif  5435  infnlbti  7316  mkvprop  7448  addnidpig  7647  zltnle  9619  zdcle  9650  btwnnz  9668  prime  9673  icc0r  10255  fznlem  10371  qltnle  10599  bcval4  11110  seq3coll  11207  swrd0g  11345  fsum3cvg  12057  fsumsplit  12086  fproddccvg  12251  fprodsplitdc  12275  bitsinv1lem  12640  2sqpwodd  12866  pockthg  13048  prmunb  13053  logbgcd1irr  15819  lgsne0  15898  eupth2lem3lem4fi  16455