Theorem pfbycase-P1.17.2SH 89

Description: Inference from pfbycase-P1.17 88

Hypotheses

Ref	Expression
pfbycase-P1.17.2SH.1	⊢ (𝜑 → 𝜓)
pfbycase-P1.17.2SH.2	⊢ (¬ 𝜑 → 𝜓)

Assertion

Ref	Expression
pfbycase-P1.17.2SH	⊢ 𝜓

Proof of Theorem pfbycase-P1.17.2SH

Step	Hyp	Ref	Expression
1		pfbycase-P1.17.2SH.2	. 2 ⊢ (¬ 𝜑 → 𝜓)
2		pfbycase-P1.17.2SH.1	. . 3 ⊢ (𝜑 → 𝜓)
3		pfbycase-P1.17 88	. . 3 ⊢ ((𝜑 → 𝜓) → ((¬ 𝜑 → 𝜓) → 𝜓))
4	2, 3	ax-MP 14	. 2 ⊢ ((¬ 𝜑 → 𝜓) → 𝜓)
5	1, 4	ax-MP 14	1 ⊢ 𝜓

Syntax hints:  ¬ wff-neg 9   → wff-imp 10

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

This theorem is referenced by:  exclmid-P2.12  152