This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )