Theorem ifnetrue

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

	Ref	Expression
Assertion	ifnetrue	|- ( ( A =/= B /\ if ( ph , A , B ) = A ) -> ph )

Proof

Step	Hyp	Ref	Expression
1		iffalse	|- ( -. ph -> if ( ph , A , B ) = B )
2	1	adantl	|- ( ( ( A =/= B /\ if ( ph , A , B ) = A ) /\ -. ph ) -> if ( ph , A , B ) = B )
3		simplr	|- ( ( ( A =/= B /\ if ( ph , A , B ) = A ) /\ -. ph ) -> if ( ph , A , B ) = A )
4		simpll	|- ( ( ( A =/= B /\ if ( ph , A , B ) = A ) /\ -. ph ) -> A =/= B )
5	3 4	eqnetrd	|- ( ( ( A =/= B /\ if ( ph , A , B ) = A ) /\ -. ph ) -> if ( ph , A , B ) =/= B )
6	5	neneqd	|- ( ( ( A =/= B /\ if ( ph , A , B ) = A ) /\ -. ph ) -> -. if ( ph , A , B ) = B )
7	2 6	condan	|- ( ( A =/= B /\ if ( ph , A , B ) = A ) -> ph )