Metamath Proof Explorer

Theorem ifnefals

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

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

Proof

Step Hyp Ref Expression
1 iftrue 
 |-  ( ph -> if ( ph , A , B ) = A )
2 1 adantl 
 |-  ( ( ( A =/= B /\ if ( ph , A , B ) = B ) /\ ph ) -> if ( ph , A , B ) = A )
3 simplr 
 |-  ( ( ( A =/= B /\ if ( ph , A , B ) = B ) /\ ph ) -> if ( ph , A , B ) = B )
4 simpll 
 |-  ( ( ( A =/= B /\ if ( ph , A , B ) = B ) /\ ph ) -> A =/= B )
5 4 necomd 
 |-  ( ( ( A =/= B /\ if ( ph , A , B ) = B ) /\ ph ) -> B =/= A )
6 3 5 eqnetrd 
 |-  ( ( ( A =/= B /\ if ( ph , A , B ) = B ) /\ ph ) -> if ( ph , A , B ) =/= A )
7 6 neneqd 
 |-  ( ( ( A =/= B /\ if ( ph , A , B ) = B ) /\ ph ) -> -. if ( ph , A , B ) = A )
8 2 7 pm2.65da 
 |-  ( ( A =/= B /\ if ( ph , A , B ) = B ) -> -. ph )