Theorem orelim-P2.11c 150

Description: '∧' Elimination Law.

This is also known as the "Proof by Cases" law.

Assertion

Ref	Expression
orelim-P2.11c	⊢ ((𝜑 → 𝜒) → ((𝜓 → 𝜒) → ((𝜑 ∨ 𝜓) → 𝜒)))

Proof of Theorem orelim-P2.11c

Step	Hyp	Ref	Expression
1		simpl-P2.9a 134	. . . . 5 ⊢ ((((𝜑 → 𝜒) ∧ (𝜓 → 𝜒)) ∧ (𝜑 ∨ 𝜓)) → ((𝜑 → 𝜒) ∧ (𝜓 → 𝜒)))
2	1	simpl-P2.9a.AC.SH 135	. . . 4 ⊢ ((((𝜑 → 𝜒) ∧ (𝜓 → 𝜒)) ∧ (𝜑 ∨ 𝜓)) → (𝜑 → 𝜒))
3		simpr-P2.9b 136	. . . . . 6 ⊢ ((((𝜑 → 𝜒) ∧ (𝜓 → 𝜒)) ∧ (𝜑 ∨ 𝜓)) → (𝜑 ∨ 𝜓))
4		df-or-D2.3 145	. . . . . . 7 ⊢ ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓))
5	4	bifwd-P2.5a.SH 112	. . . . . 6 ⊢ ((𝜑 ∨ 𝜓) → (¬ 𝜑 → 𝜓))
6	3, 5	syl-P1.2 34	. . . . 5 ⊢ ((((𝜑 → 𝜒) ∧ (𝜓 → 𝜒)) ∧ (𝜑 ∨ 𝜓)) → (¬ 𝜑 → 𝜓))
7	1	simpr-P2.9b.AC.SH 137	. . . . 5 ⊢ ((((𝜑 → 𝜒) ∧ (𝜓 → 𝜒)) ∧ (𝜑 ∨ 𝜓)) → (𝜓 → 𝜒))
8	6, 7	sylt-P1.9.AC.2SH 62	. . . 4 ⊢ ((((𝜑 → 𝜒) ∧ (𝜓 → 𝜒)) ∧ (𝜑 ∨ 𝜓)) → (¬ 𝜑 → 𝜒))
9	2, 8	pfbycase-P1.17.AC.2SH 90	. . 3 ⊢ ((((𝜑 → 𝜒) ∧ (𝜓 → 𝜒)) ∧ (𝜑 ∨ 𝜓)) → 𝜒)
10	9	export-P2.10b.SH 143	. 2 ⊢ (((𝜑 → 𝜒) ∧ (𝜓 → 𝜒)) → ((𝜑 ∨ 𝜓) → 𝜒))
11	10	export-P2.10b.SH 143	1 ⊢ ((𝜑 → 𝜒) → ((𝜓 → 𝜒) → ((𝜑 ∨ 𝜓) → 𝜒)))

Syntax hints:  ¬ wff-neg 9   → 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:  orelim-P2.11c.AC.3SH  151