Theorem 1fpid3

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.)

Hypothesis
1fpid3.1
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
Conclusion
\( \vdash \operatorname{if} ( \varphi , \psi , \chi ) \rightarrow \chi \)
Proof
l0
df-ifp
\( \vdash \operatorname{if} ( \varphi , \psi , \chi ) \leftrightarrow \varphi \wedge \psi \vee \neg \varphi \wedge \chi \)
l1
1fpid3.1
simpr
jaoi l1 _
\( \vdash \varphi \wedge \psi \vee \neg \varphi \wedge \chi \rightarrow \chi \)
sylbi l0 _