Theorem iftrueb

Description: When the branches are not equal, an "if" condition results in the first branch if and only if its condition is true. (Contributed by SN, 16-Oct-2025)

	Ref	Expression
Assertion	iftrueb	$$⊢A\ne B\to \left(if\left(\phi ,A,B\right)=A\leftrightarrow \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		necom	$$⊢A\ne B\leftrightarrow B\ne A$$
2	1	biimpi	$$⊢A\ne B\to B\ne A$$
3		iffalse	$$⊢\neg \phi \to if\left(\phi ,A,B\right)=B$$
4	3	neeq1d	$$⊢\neg \phi \to \left(if\left(\phi ,A,B\right)\ne A\leftrightarrow B\ne A\right)$$
5	2 4	syl5ibrcom	$$⊢A\ne B\to \left(\neg \phi \to if\left(\phi ,A,B\right)\ne A\right)$$
6	5	necon4bd	$$⊢A\ne B\to \left(if\left(\phi ,A,B\right)=A\to \phi \right)$$
7		iftrue	$$⊢\phi \to if\left(\phi ,A,B\right)=A$$
8	6 7	impbid1	$$⊢A\ne B\to \left(if\left(\phi ,A,B\right)=A\leftrightarrow \phi \right)$$