Theorem ifnetrue

Description: Deduce truth from a conditional operator value. (Contributed by Thierry Arnoux, 20-Feb-2025)

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

Proof

Step	Hyp	Ref	Expression
1		iffalse	$$⊢\neg \phi \to if\left(\phi ,A,B\right)=B$$
2	1	adantl	$$⊢\left(\left(A\ne B\wedge if\left(\phi ,A,B\right)=A\right)\wedge \neg \phi \right)\to if\left(\phi ,A,B\right)=B$$
3		simplr	$$⊢\left(\left(A\ne B\wedge if\left(\phi ,A,B\right)=A\right)\wedge \neg \phi \right)\to if\left(\phi ,A,B\right)=A$$
4		simpll	$$⊢\left(\left(A\ne B\wedge if\left(\phi ,A,B\right)=A\right)\wedge \neg \phi \right)\to A\ne B$$
5	3 4	eqnetrd	$$⊢\left(\left(A\ne B\wedge if\left(\phi ,A,B\right)=A\right)\wedge \neg \phi \right)\to if\left(\phi ,A,B\right)\ne B$$
6	5	neneqd	$$⊢\left(\left(A\ne B\wedge if\left(\phi ,A,B\right)=A\right)\wedge \neg \phi \right)\to \neg if\left(\phi ,A,B\right)=B$$
7	2 6	condan	$$⊢\left(A\ne B\wedge if\left(\phi ,A,B\right)=A\right)\to \phi$$