Theorem ifpbi23d

Equivalence deduction for conditional operator for propositions. Convenience theorem for a frequent case. (Contributed by Wolf Lammen, 28-Apr-2024.)

Hypotheses
ifpbi23d.1
\( \vdash \varphi \rightarrow (\chi \leftrightarrow \eta) \)
ifpbi23d.2
\( \vdash \varphi \rightarrow (\theta \leftrightarrow \zeta) \)
Conclusion
\( \vdash \varphi \rightarrow (\operatorname{if} ( \psi , \chi , \theta ) \leftrightarrow \operatorname{if} ( \psi , \eta , \zeta )) \)
Proof
l0
biidd
l1
ifpbi23d.1
ifpbi23d.2
ifpbi123d l0 l1 _