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  2180  necon2ad  2471  necon2bd  2472  minel  3574  nlimsucg  4693  poirr2  5160  funun  5402  imadif  5441  infnlbti  7330  mkvprop  7462  addnidpig  7667  zltnle  9643  zdcle  9674  btwnnz  9693  prime  9698  icc0r  10281  fznlem  10398  qltnle  10630  bcval4  11142  seq3coll  11242  swrd0g  11380  fsum3cvg  12092  fsumsplit  12121  fproddccvg  12286  fprodsplitdc  12310  bitsinv1lem  12675  2sqpwodd  12901  pockthg  13083  prmunb  13088  ballotfilemfc0  13179  ballotfilemfcc  13180  ballotfilemirc  13222  logbgcd1irr  15961  lgsne0  16040  eupth2lem3lem4fi  16597