This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database GUIDES AND MISCELLANEA Guides (conventions, explanations, and examples) Natural deduction examples ex-natded5.13-2
Description: A more efficient proof of Theorem 5.13 of Clemente p. 20. Compare
with ex-natded5.13 . (Contributed by Mario Carneiro , 9-Feb-2017)
(Proof modification is discouraged.) (New usage is discouraged.)
Ref
Expression
Hypotheses
ex-natded5.13.1 ⊢ ( 𝜑 → ( 𝜓 ∨ 𝜒 ) )
ex-natded5.13.2 ⊢ ( 𝜑 → ( 𝜓 → 𝜃 ) )
ex-natded5.13.3 ⊢ ( 𝜑 → ( ¬ 𝜏 → ¬ 𝜒 ) )
Assertion
ex-natded5.13-2 ⊢ ( 𝜑 → ( 𝜃 ∨ 𝜏 ) )
Proof
Step
Hyp
Ref
Expression
1
ex-natded5.13.1 ⊢ ( 𝜑 → ( 𝜓 ∨ 𝜒 ) )
2
ex-natded5.13.2 ⊢ ( 𝜑 → ( 𝜓 → 𝜃 ) )
3
ex-natded5.13.3 ⊢ ( 𝜑 → ( ¬ 𝜏 → ¬ 𝜒 ) )
4
3
con4d ⊢ ( 𝜑 → ( 𝜒 → 𝜏 ) )
5
2 4
orim12d ⊢ ( 𝜑 → ( ( 𝜓 ∨ 𝜒 ) → ( 𝜃 ∨ 𝜏 ) ) )
6
1 5
mpd ⊢ ( 𝜑 → ( 𝜃 ∨ 𝜏 ) )