Metamath Proof Explorer

Theorem ifle

Description: An if statement transforms an implication into an inequality of terms. (Contributed by Mario Carneiro, 31-Aug-2014)

Ref Expression
Assertion ifle 
|- ( ( ( A e. RR /\ B e. RR /\ B <_ A ) /\ ( ph -> ps ) ) -> if ( ph , A , B ) <_ if ( ps , A , B ) )

Proof

Step Hyp Ref Expression
1 simpll1 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ B <_ A ) /\ ( ph -> ps ) ) /\ ph ) -> A e. RR )
2 1 leidd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ B <_ A ) /\ ( ph -> ps ) ) /\ ph ) -> A <_ A )
3 iftrue 
 |-  ( ph -> if ( ph , A , B ) = A )
4 3 adantl 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ B <_ A ) /\ ( ph -> ps ) ) /\ ph ) -> if ( ph , A , B ) = A )
5 id 
 |-  ( ( ph -> ps ) -> ( ph -> ps ) )
6 5 imp 
 |-  ( ( ( ph -> ps ) /\ ph ) -> ps )
7 6 adantll 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ B <_ A ) /\ ( ph -> ps ) ) /\ ph ) -> ps )
8 7 iftrued 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ B <_ A ) /\ ( ph -> ps ) ) /\ ph ) -> if ( ps , A , B ) = A )
9 2 4 8 3brtr4d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ B <_ A ) /\ ( ph -> ps ) ) /\ ph ) -> if ( ph , A , B ) <_ if ( ps , A , B ) )
10 iffalse 
 |-  ( -. ph -> if ( ph , A , B ) = B )
11 10 adantl 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ B <_ A ) /\ ( ph -> ps ) ) /\ -. ph ) -> if ( ph , A , B ) = B )
12 simpll3 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ B <_ A ) /\ ( ph -> ps ) ) /\ -. ph ) -> B <_ A )
13 simpll2 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ B <_ A ) /\ ( ph -> ps ) ) /\ -. ph ) -> B e. RR )
14 13 leidd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ B <_ A ) /\ ( ph -> ps ) ) /\ -. ph ) -> B <_ B )
15 breq2 
 |-  ( A = if ( ps , A , B ) -> ( B <_ A <-> B <_ if ( ps , A , B ) ) )
16 breq2 
 |-  ( B = if ( ps , A , B ) -> ( B <_ B <-> B <_ if ( ps , A , B ) ) )
17 15 16 ifboth 
 |-  ( ( B <_ A /\ B <_ B ) -> B <_ if ( ps , A , B ) )
18 12 14 17 syl2anc 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ B <_ A ) /\ ( ph -> ps ) ) /\ -. ph ) -> B <_ if ( ps , A , B ) )
19 11 18 eqbrtrd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ B <_ A ) /\ ( ph -> ps ) ) /\ -. ph ) -> if ( ph , A , B ) <_ if ( ps , A , B ) )
20 9 19 pm2.61dan 
 |-  ( ( ( A e. RR /\ B e. RR /\ B <_ A ) /\ ( ph -> ps ) ) -> if ( ph , A , B ) <_ if ( ps , A , B ) )