Theorem con2d 83

Description: A contraposition deduction.

Hypothesis

Ref	Expression
con2d.1	⊢ (φ → (ψ → ¬ χ))

Assertion

Ref	Expression
con2d	⊢ (φ → (χ → ¬ ψ))

Proof of Theorem con2d

Step	Hyp	Ref	Expression
1		con2d.1	. 2 ⊢ (φ → (ψ → ¬ χ))
2		con2 82	. 2 ⊢ ((ψ → ¬ χ) → (χ → ¬ ψ))
3	1, 2	syl 12	1 ⊢ (φ → (χ → ¬ ψ))

Syntax hints:  ¬ wn 1   → wi 2

This theorem is referenced by:  con3 86  mt2i 97  mt2d 98  pm3.2im 107  pm2.65 115  cla4egf 1395  minel 1743  sotric 2148  supmo 2156  supnub 2162  tz7.2 2183  nordeq 2218  onnminsb 2271  oneqmin 2273  onminex 2275  limsssuc 2362  funun 2700  imadif 2714  tfrlem10 2958  tz7.48lem 2993  pssinf 3422  unblem1 3431  eirrv 3449  inf3lem6 3469  aceq5 3563  cardne 3637  carddom 3642  ondomcard 3663  cardmin 3666  alephnbtwn 3674  addnidpi 3822  genpnnp 3902  lt0nnn0 4549  nn0ge0t 4550  normgt0t 5078  stadd 5687  stadd3 5689  cvnsymt 5722  cvntrt 5724  atcvat 5771

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

metamath.org