Theorem ifpbi123d
Equivalence deduction for conditional operator for propositions.
(Contributed by AV, 30-Dec-2020.) (Proof shortened by Wolf Lammen,
17-Apr-2024.)
Hypotheses
ifpbi123d.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \tau) \)
ifpbi123d.2
\( \vdash \varphi \rightarrow (\chi \leftrightarrow \eta) \)
ifpbi123d.3
\( \vdash \varphi \rightarrow (\theta \leftrightarrow \zeta) \)
Conclusion
\( \vdash \varphi \rightarrow (\operatorname{if} ( \psi , \chi , \theta ) \leftrightarrow \operatorname{if} ( \tau , \eta , \zeta )) \)
Proof
l0
ifpbi123d.1
ifpbi123d.2
l2
imbi12d l0 _
l3
ifpbi123d.1
ifpbi123d.3
orbi12d l3 _
l6
anbi12d l2 _
\( \vdash \varphi \rightarrow ((\psi \rightarrow \chi) \wedge (\psi \vee \theta) \leftrightarrow (\tau \rightarrow \eta) \wedge (\tau \vee \zeta)) \)
l7
dfifp3
\( \vdash \operatorname{if} ( \psi , \chi , \theta ) \leftrightarrow (\psi \rightarrow \chi) \wedge (\psi \vee \theta) \)
dfifp3
\( \vdash \operatorname{if} ( \tau , \eta , \zeta ) \leftrightarrow (\tau \rightarrow \eta) \wedge (\tau \vee \zeta) \)
3bitr4g l6 l7 _