Theorem ifnefals

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

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

Proof

Step	Hyp	Ref	Expression
1		iftrue	$$⊢\phi \to if\left(\phi ,A,B\right)=A$$
2	1	adantl	$$⊢\left(\left(A\ne B\wedge if\left(\phi ,A,B\right)=B\right)\wedge \phi \right)\to if\left(\phi ,A,B\right)=A$$
3		simplr	$$⊢\left(\left(A\ne B\wedge if\left(\phi ,A,B\right)=B\right)\wedge \phi \right)\to if\left(\phi ,A,B\right)=B$$
4		simpll	$$⊢\left(\left(A\ne B\wedge if\left(\phi ,A,B\right)=B\right)\wedge \phi \right)\to A\ne B$$
5	4	necomd	$$⊢\left(\left(A\ne B\wedge if\left(\phi ,A,B\right)=B\right)\wedge \phi \right)\to B\ne A$$
6	3 5	eqnetrd	$$⊢\left(\left(A\ne B\wedge if\left(\phi ,A,B\right)=B\right)\wedge \phi \right)\to if\left(\phi ,A,B\right)\ne A$$
7	6	neneqd	$$⊢\left(\left(A\ne B\wedge if\left(\phi ,A,B\right)=B\right)\wedge \phi \right)\to \neg if\left(\phi ,A,B\right)=A$$
8	2 7	pm2.65da	$$⊢\left(A\ne B\wedge if\left(\phi ,A,B\right)=B\right)\to \neg \phi$$