Theorem ndore-P3.12 177

Description: Natural Deduction: '∨' Elimination Rule.

If...

1.) after assuming '𝜑' we deduce '𝜒',

2.) after assuming '𝜓' we also deduce '𝜒', and

3.) we know that either '𝜑' or '𝜓' holds,

then we can deduce '𝜒' with the case assumptions, '𝜑' and '𝜓', discharged.

Hypotheses

Ref	Expression
ndore-P3.12.1	⊢ ((𝛾 ∧ 𝜑) → 𝜒)
ndore-P3.12.2	⊢ ((𝛾 ∧ 𝜓) → 𝜒)
ndore-P3.12.3	⊢ (𝛾 → (𝜑 ∨ 𝜓))

Assertion

Ref	Expression
ndore-P3.12	⊢ (𝛾 → 𝜒)

Proof of Theorem ndore-P3.12

Step	Hyp	Ref	Expression
1		ndore-P3.12.1	. . 3 ⊢ ((𝛾 ∧ 𝜑) → 𝜒)
2	1	export-P2.10b.SH 143	. 2 ⊢ (𝛾 → (𝜑 → 𝜒))
3		ndore-P3.12.2	. . 3 ⊢ ((𝛾 ∧ 𝜓) → 𝜒)
4	3	export-P2.10b.SH 143	. 2 ⊢ (𝛾 → (𝜓 → 𝜒))
5		ndore-P3.12.3	. 2 ⊢ (𝛾 → (𝜑 ∨ 𝜓))
6	2, 4, 5	orelim-P2.11c.AC.3SH 151	1 ⊢ (𝛾 → 𝜒)

Syntax hints:   → wff-imp 10   ∧ wff-and 132   ∨ wff-or 144

This theorem was proved from axioms:  ax-L1 11  ax-L2 12  ax-L3 13  ax-MP 14

This theorem depends on definitions:  df-bi-D2.1 107  df-and-D2.2 133  df-or-D2.3 145

This theorem is referenced by:  rcp-NDORE1  234  rcp-NDORE2  235  rcp-NDORE3  236  rcp-NDORE4  237  rcp-NDORE5  238  dnege-P3.30  276