Theorem con2d 633

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 624	. . . 4 ⊢ (¬ 𝜒 → (𝜒 → ¬ 𝜓))
3	1, 2	syl6 33	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → ¬ 𝜓)))
4	3	com23 78	. 2 ⊢ (𝜑 → (𝜒 → (𝜓 → ¬ 𝜓)))
5		pm2.01 625	. 2 ⊢ ((𝜓 → ¬ 𝜓) → ¬ 𝜓)
6	4, 5	syl6 33	1 ⊢ (𝜑 → (𝜒 → ¬ 𝜓))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 623  ax-in2 624

This theorem is used by:  mt2d  634  con3d  640  pm3.2im  646  con2  652  pm2.65  669  con1biimdc  885  exists2  2184  necon2ad  2477  necon2bd  2478  minel  3586  nlimsucg  4715  poirr2  5183  funun  5425  imadif  5464  infnlbti  7373  mkvprop  7505  addnidpig  7710  zltnle  9702  zdcle  9733  btwnnz  9752  prime  9757  icc0r  10346  fznlem  10463  qltnle  10696  bcval4  11213  hashf1  11310  seq3coll  11317  swrd0g  11455  fsum3cvg  12171  fsumsplit  12200  fproddccvg  12365  fprodsplitdc  12389  bitsinv1lem  12754  2sqpwodd  12982  pockthg  13166  prmunb  13171  ballotfilemfc0  13291  ballotfilemfcc  13292  ballotfilemirc  13334  logbgcd1irr  16215  chtqub  16308  lgsne0  16374  eupth2lem3lem4fi  16931