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 ⊢ (𝜑 → (𝜒 → ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 623  ax-in2 624

This theorem is referenced by:  mt2d  634  con3d  640  pm3.2im  646  con2  652  pm2.65  669  con1biimdc  885  exists2  2184  necon2ad  2477  necon2bd  2478  minel  3586  nlimsucg  4711  poirr2  5178  funun  5420  imadif  5459  infnlbti  7360  mkvprop  7492  addnidpig  7697  zltnle  9673  zdcle  9704  btwnnz  9723  prime  9728  icc0r  10311  fznlem  10428  qltnle  10661  bcval4  11173  hashf1  11270  seq3coll  11277  swrd0g  11415  fsum3cvg  12128  fsumsplit  12157  fproddccvg  12322  fprodsplitdc  12346  bitsinv1lem  12711  2sqpwodd  12937  pockthg  13119  prmunb  13124  ballotfilemfc0  13215  ballotfilemfcc  13216  ballotfilemirc  13258  logbgcd1irr  16052  lgsne0  16140  eupth2lem3lem4fi  16697