Theorem con2d 627

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 618	. . . 4 ⊢ (¬ 𝜒 → (𝜒 → ¬ 𝜓))
3	1, 2	syl6 33	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → ¬ 𝜓)))
4	3	com23 78	. 2 ⊢ (𝜑 → (𝜒 → (𝜓 → ¬ 𝜓)))
5		pm2.01 619	. 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 617  ax-in2 618

This theorem is referenced by:  mt2d  628  con3d  634  pm3.2im  640  con2  646  pm2.65  663  con1biimdc  877  exists2  2155  necon2ad  2437  necon2bd  2438  minel  3533  nlimsucg  4635  poirr2  5097  funun  5338  imadif  5377  infnlbti  7161  mkvprop  7293  addnidpig  7491  zltnle  9460  zdcle  9491  btwnnz  9509  prime  9514  icc0r  10090  fznlem  10205  qltnle  10430  bcval4  10941  seq3coll  11031  swrd0g  11158  fsum3cvg  11855  fsumsplit  11884  fproddccvg  12049  fprodsplitdc  12073  bitsinv1lem  12438  2sqpwodd  12664  pockthg  12846  prmunb  12851  logbgcd1irr  15606  lgsne0  15682