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

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 )