Metamath Proof Explorer

Theorem pm4.83

Description: Theorem *4.83 of WhiteheadRussell p. 122. (Contributed by NM, 3-Jan-2005)

		Ref	Expression
	Assertion	pm4.83	$⊢ ((φ \to ψ) \land (\neg φ \to ψ)) \leftrightarrow ψ$

Step	Hyp	Ref	Expression
1		exmid	$⊢ (φ \lor \neg φ)$
2	1	a1bi	$⊢ ψ \leftrightarrow ((φ \lor \neg φ) \to ψ)$
3		jaob	$⊢ ((φ \lor \neg φ) \to ψ) \leftrightarrow ((φ \to ψ) \land (\neg φ \to ψ))$
4	2 3	bitr2i	$⊢ ((φ \to ψ) \land (\neg φ \to ψ)) \leftrightarrow ψ$