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	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜒 )
Assertion	1fpid3	⊢ ( if- ( 𝜑 , 𝜓 , 𝜒 ) → 𝜒 )

Proof

Step	Hyp	Ref	Expression
1		1fpid3.1	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜒 )
2		df-ifp	⊢ ( if- ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) )
3		simpr	⊢ ( ( ¬ 𝜑 ∧ 𝜒 ) → 𝜒 )
4	1 3	jaoi	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) → 𝜒 )
5	2 4	sylbi	⊢ ( if- ( 𝜑 , 𝜓 , 𝜒 ) → 𝜒 )