Theorem orelim-P2.11c.AC.3SH 151

Description: Deductive Form of orelim-P2.11c 150.

Hypotheses

Ref	Expression
orelim-P2.11c.AC.3SH.1	⊢ (𝛾 → (𝜑 → 𝜒))
orelim-P2.11c.AC.3SH.2	⊢ (𝛾 → (𝜓 → 𝜒))
orelim-P2.11c.AC.3SH.3	⊢ (𝛾 → (𝜑 ∨ 𝜓))

Assertion

Ref	Expression
orelim-P2.11c.AC.3SH	⊢ (𝛾 → 𝜒)

Proof of Theorem orelim-P2.11c.AC.3SH

Step	Hyp	Ref	Expression
1		orelim-P2.11c.AC.3SH.3	. 2 ⊢ (𝛾 → (𝜑 ∨ 𝜓))
2		orelim-P2.11c.AC.3SH.2	. . . 4 ⊢ (𝛾 → (𝜓 → 𝜒))
3		orelim-P2.11c.AC.3SH.1	. . . . . 6 ⊢ (𝛾 → (𝜑 → 𝜒))
4		orelim-P2.11c 150	. . . . . . . 8 ⊢ ((𝜑 → 𝜒) → ((𝜓 → 𝜒) → ((𝜑 ∨ 𝜓) → 𝜒)))
5	4	axL1.SH 30	. . . . . . 7 ⊢ (𝛾 → ((𝜑 → 𝜒) → ((𝜓 → 𝜒) → ((𝜑 ∨ 𝜓) → 𝜒))))
6	5	rcp-FR1.SH 40	. . . . . 6 ⊢ ((𝛾 → (𝜑 → 𝜒)) → (𝛾 → ((𝜓 → 𝜒) → ((𝜑 ∨ 𝜓) → 𝜒))))
7	3, 6	ax-MP 14	. . . . 5 ⊢ (𝛾 → ((𝜓 → 𝜒) → ((𝜑 ∨ 𝜓) → 𝜒)))
8	7	rcp-FR1.SH 40	. . . 4 ⊢ ((𝛾 → (𝜓 → 𝜒)) → (𝛾 → ((𝜑 ∨ 𝜓) → 𝜒)))
9	2, 8	ax-MP 14	. . 3 ⊢ (𝛾 → ((𝜑 ∨ 𝜓) → 𝜒))
10	9	axL2.SH 31	. 2 ⊢ ((𝛾 → (𝜑 ∨ 𝜓)) → (𝛾 → 𝜒))
11	1, 10	ax-MP 14	1 ⊢ (𝛾 → 𝜒)

Syntax hints:   → wff-imp 10   ∨ 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:  ndore-P3.12  177