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

Metamath Proof Explorer

Theorem ifeq12da

Description: Equivalence deduction for conditional operators. (Contributed by Wolf Lammen, 24-Jun-2021)

Ref Expression
Hypotheses ifeq12da.1 
|- ( ( ph /\ ps ) -> A = C )
ifeq12da.2 
|- ( ( ph /\ -. ps ) -> B = D )
Assertion ifeq12da 
|- ( ph -> if ( ps , A , B ) = if ( ps , C , D ) )

Proof

Step Hyp Ref Expression
1 ifeq12da.1 
 |-  ( ( ph /\ ps ) -> A = C )
2 ifeq12da.2 
 |-  ( ( ph /\ -. ps ) -> B = D )
3 1 ifeq1da 
 |-  ( ph -> if ( ps , A , B ) = if ( ps , C , B ) )
4 iftrue 
 |-  ( ps -> if ( ps , C , B ) = C )
5 iftrue 
 |-  ( ps -> if ( ps , C , D ) = C )
6 4 5 eqtr4d 
 |-  ( ps -> if ( ps , C , B ) = if ( ps , C , D ) )
7 3 6 sylan9eq 
 |-  ( ( ph /\ ps ) -> if ( ps , A , B ) = if ( ps , C , D ) )
8 2 ifeq2da 
 |-  ( ph -> if ( ps , A , B ) = if ( ps , A , D ) )
9 iffalse 
 |-  ( -. ps -> if ( ps , A , D ) = D )
10 iffalse 
 |-  ( -. ps -> if ( ps , C , D ) = D )
11 9 10 eqtr4d 
 |-  ( -. ps -> if ( ps , A , D ) = if ( ps , C , D ) )
12 8 11 sylan9eq 
 |-  ( ( ph /\ -. ps ) -> if ( ps , A , B ) = if ( ps , C , D ) )
13 7 12 pm2.61dan 
 |-  ( ph -> if ( ps , A , B ) = if ( ps , C , D ) )