Theorem a3d 75

Description: Deduction derived from axiom ax-3 6.

Hypothesis

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

Assertion

Ref	Expression
a3d	⊢ (φ → (χ → ψ))

Proof of Theorem a3d

Step	Hyp	Ref	Expression
1		a3d.1	. 2 ⊢ (φ → (¬ ψ → ¬ χ))
2		ax-3 6	. 2 ⊢ ((¬ ψ → ¬ χ) → (χ → ψ))
3	1, 2	syl 10	1 ⊢ (φ → (χ → ψ))

Syntax hints:  ¬ wn 2   → wi 3

This theorem is referenced by:  pm2.21 76  pm2.21d 78  pm2.18 81  con2 90  con1 92  pm2.521 103  mt4d 115  ax4 970  necon4ad 1623  necon4bd 1624  cla42gv 1861  cla43gv 1863  ra4esbca 1995  iununi 2611  limom 3141  isomin 3890  preleq 4583  sdomel 4827  cardsdomel 4832  ltapr 5131  suplem2pr 5142  lt2msq 5837  qsqueeze 6226  om2uzlt2 6244  nn0opth 6604  infpnlem1 7457  infxpidmlem12 7514  atcv0eq 10243  iintlem1 10512

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

Copyright terms: Public domain