This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 1fpid3

Description: The value of the conditional operator for propositions is its third argument if the first and second argument imply the third argument. (Contributed by AV, 4-Apr-2021)

		Ref	Expression
	Hypothesis	1fpid3.1	$⊢ (φ \land ψ) \to χ$
	Assertion	1fpid3	$⊢ if- (φ, ψ, χ) \to χ$

Proof

Step	Hyp	Ref	Expression
1		1fpid3.1	$⊢ (φ \land ψ) \to χ$
2		df-ifp	$⊢ if- (φ, ψ, χ) \leftrightarrow ((φ \land ψ) \lor (\neg φ \land χ))$
3		simpr	$⊢ (\neg φ \land χ) \to χ$
4	1 3	jaoi	$⊢ ((φ \land ψ) \lor (\neg φ \land χ)) \to χ$
5	2 4	sylbi	$⊢ if- (φ, ψ, χ) \to χ$