Theorem bibiad
Eliminate an hypothesis \( \theta \) in a biconditional. (Contributed by
Thierry Arnoux, 4-May-2025.)
Hypotheses
bibiad.1
\( \vdash \varphi \wedge \psi \rightarrow \theta \)
bibiad.2
\( \vdash \varphi \wedge \chi \rightarrow \theta \)
bibiad.3
\( \vdash \varphi \wedge \theta \rightarrow (\psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
Proof
l0
simpl
\( \vdash \varphi \wedge \psi \rightarrow \varphi \)
l1
bibiad.1
\( \vdash \varphi \wedge \psi \rightarrow \theta \)
l2
simpr
\( \vdash \varphi \wedge \psi \rightarrow \psi \)
bibiad.3
biimpa _
\( \vdash \varphi \wedge \theta \wedge \psi \rightarrow \chi \)
l5
syl21anc l0 l1 l2 _
l6
simpl
\( \vdash \varphi \wedge \chi \rightarrow \varphi \)
l7
bibiad.2
\( \vdash \varphi \wedge \chi \rightarrow \theta \)
l8
simpr
\( \vdash \varphi \wedge \chi \rightarrow \chi \)
bibiad.3
biimpar _
\( \vdash \varphi \wedge \theta \wedge \chi \rightarrow \psi \)
syl21anc l6 l7 l8 _
impbida l5 _