Metamath Proof Explorer


Theorem ifeq3da

Description: Given an expression C containing if ( ps , E , F ) , substitute (hypotheses .1 and .2) and evaluate (hypotheses .3 and .4) it for both cases at the same time. (Contributed by Thierry Arnoux, 13-Dec-2021)

Ref Expression
Hypotheses ifeq3da.1
|- ( if ( ps , E , F ) = E -> C = G )
ifeq3da.2
|- ( if ( ps , E , F ) = F -> C = H )
ifeq3da.3
|- ( ph -> G = A )
ifeq3da.4
|- ( ph -> H = B )
Assertion ifeq3da
|- ( ph -> if ( ps , A , B ) = C )

Proof

Step Hyp Ref Expression
1 ifeq3da.1
 |-  ( if ( ps , E , F ) = E -> C = G )
2 ifeq3da.2
 |-  ( if ( ps , E , F ) = F -> C = H )
3 ifeq3da.3
 |-  ( ph -> G = A )
4 ifeq3da.4
 |-  ( ph -> H = B )
5 iftrue
 |-  ( ps -> if ( ps , E , F ) = E )
6 5 1 syl
 |-  ( ps -> C = G )
7 6 adantl
 |-  ( ( ph /\ ps ) -> C = G )
8 3 adantr
 |-  ( ( ph /\ ps ) -> G = A )
9 7 8 eqtr2d
 |-  ( ( ph /\ ps ) -> A = C )
10 iffalse
 |-  ( -. ps -> if ( ps , E , F ) = F )
11 10 2 syl
 |-  ( -. ps -> C = H )
12 11 adantl
 |-  ( ( ph /\ -. ps ) -> C = H )
13 4 adantr
 |-  ( ( ph /\ -. ps ) -> H = B )
14 12 13 eqtr2d
 |-  ( ( ph /\ -. ps ) -> B = C )
15 9 14 ifeqda
 |-  ( ph -> if ( ps , A , B ) = C )