Theorem hadbi123d
Equality theorem for the adder sum. (Contributed by Mario Carneiro,
4-Sep-2016.)
Hypotheses
hadbid.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
hadbid.2
\( \vdash \varphi \rightarrow (\theta \leftrightarrow \tau) \)
hadbid.3
\( \vdash \varphi \rightarrow (\eta \leftrightarrow \zeta) \)
Conclusion
\( \vdash \varphi \rightarrow (\text{ hadd } ( \psi , \theta , \eta ) \leftrightarrow \text{ hadd } ( \chi , \tau , \zeta )) \)
Proof
l0
hadbid.1
hadbid.2
l2
xorbi12d l0 _
hadbid.3
l4
xorbi12d l2 _
\( \vdash \varphi \rightarrow ((\psi \veebar \theta) \veebar \eta \leftrightarrow (\chi \veebar \tau) \veebar \zeta) \)
l5
df-had
\( \vdash \text{ hadd } ( \psi , \theta , \eta ) \leftrightarrow (\psi \veebar \theta) \veebar \eta \)
df-had
\( \vdash \text{ hadd } ( \chi , \tau , \zeta ) \leftrightarrow (\chi \veebar \tau) \veebar \zeta \)
3bitr4g l4 l5 _