Theorem mtord 641

Description: A modus tollens deduction involving disjunction. (Contributed by Jeff Hankins, 15-Jul-2009.)

Hypotheses

Ref	Expression
mtord.1	⊢ (φ → ¬ χ)
mtord.2	⊢ (φ → ¬ θ)
mtord.3	⊢ (φ → (ψ → (χ ∨ θ)))

Assertion

Ref	Expression
mtord	⊢ (φ → ¬ ψ)

Proof of Theorem mtord

Step	Hyp	Ref	Expression
1		mtord.2	. 2 ⊢ (φ → ¬ θ)
2		mtord.1	. . 3 ⊢ (φ → ¬ χ)
3		mtord.3	. . . 4 ⊢ (φ → (ψ → (χ ∨ θ)))
4		df-or 359	. . . 4 ⊢ ((χ ∨ θ) ↔ (¬ χ → θ))
5	3, 4	syl6ib 217	. . 3 ⊢ (φ → (ψ → (¬ χ → θ)))
6	2, 5	mpid 37	. 2 ⊢ (φ → (ψ → θ))
7	1, 6	mtod 168	1 ⊢ (φ → ¬ ψ)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∨ wo 357

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 177  df-or 359

This theorem is used by: (None)