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	|- ( ( ph /\ ps ) -> ch )
Assertion	1fpid3	|- ( if- ( ph , ps , ch ) -> ch )

Proof

Step	Hyp	Ref	Expression
1		1fpid3.1	|- ( ( ph /\ ps ) -> ch )
2		df-ifp	|- ( if- ( ph , ps , ch ) <-> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) )
3		simpr	|- ( ( -. ph /\ ch ) -> ch )
4	1 3	jaoi	|- ( ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) -> ch )
5	2 4	sylbi	|- ( if- ( ph , ps , ch ) -> ch )