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  3572  nlimsucg  4690  poirr2  5157  funun  5399  imadif  5438  infnlbti  7319  mkvprop  7451  addnidpig  7656  zltnle  9628  zdcle  9659  btwnnz  9678  prime  9683  icc0r  10265  fznlem  10381  qltnle  10610  bcval4  11122  seq3coll  11222  swrd0g  11360  fsum3cvg  12072  fsumsplit  12101  fproddccvg  12266  fprodsplitdc  12290  bitsinv1lem  12655  2sqpwodd  12881  pockthg  13063  prmunb  13068  ballotfilemfc0  13157  ballotfilemfcc  13158  logbgcd1irr  15881  lgsne0  15960  eupth2lem3lem4fi  16517