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  4713  poirr2  5180  funun  5422  imadif  5461  infnlbti  7366  mkvprop  7498  addnidpig  7703  zltnle  9692  zdcle  9723  btwnnz  9742  prime  9747  icc0r  10330  fznlem  10447  qltnle  10680  bcval4  11192  hashf1  11289  seq3coll  11296  swrd0g  11434  fsum3cvg  12147  fsumsplit  12176  fproddccvg  12341  fprodsplitdc  12365  bitsinv1lem  12730  2sqpwodd  12956  pockthg  13138  prmunb  13143  ballotfilemfc0  13234  ballotfilemfcc  13235  ballotfilemirc  13277  logbgcd1irr  16075  lgsne0  16169  eupth2lem3lem4fi  16726