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 ( 𝜓 , 𝐸 , 𝐹 ) = 𝐸 → 𝐶 = 𝐺 )
		ifeq3da.2	⊢ ( if ( 𝜓 , 𝐸 , 𝐹 ) = 𝐹 → 𝐶 = 𝐻 )
		ifeq3da.3	⊢ ( 𝜑 → 𝐺 = 𝐴 )
		ifeq3da.4	⊢ ( 𝜑 → 𝐻 = 𝐵 )
	Assertion	ifeq3da	⊢ ( 𝜑 → if ( 𝜓 , 𝐴 , 𝐵 ) = 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		ifeq3da.1	⊢ ( if ( 𝜓 , 𝐸 , 𝐹 ) = 𝐸 → 𝐶 = 𝐺 )
2		ifeq3da.2	⊢ ( if ( 𝜓 , 𝐸 , 𝐹 ) = 𝐹 → 𝐶 = 𝐻 )
3		ifeq3da.3	⊢ ( 𝜑 → 𝐺 = 𝐴 )
4		ifeq3da.4	⊢ ( 𝜑 → 𝐻 = 𝐵 )
5		iftrue	⊢ ( 𝜓 → if ( 𝜓 , 𝐸 , 𝐹 ) = 𝐸 )
6	5 1	syl	⊢ ( 𝜓 → 𝐶 = 𝐺 )
7	6	adantl	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐶 = 𝐺 )
8	3	adantr	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐺 = 𝐴 )
9	7 8	eqtr2d	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐴 = 𝐶 )
10		iffalse	⊢ ( ¬ 𝜓 → if ( 𝜓 , 𝐸 , 𝐹 ) = 𝐹 )
11	10 2	syl	⊢ ( ¬ 𝜓 → 𝐶 = 𝐻 )
12	11	adantl	⊢ ( ( 𝜑 ∧ ¬ 𝜓 ) → 𝐶 = 𝐻 )
13	4	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝜓 ) → 𝐻 = 𝐵 )
14	12 13	eqtr2d	⊢ ( ( 𝜑 ∧ ¬ 𝜓 ) → 𝐵 = 𝐶 )
15	9 14	ifeqda	⊢ ( 𝜑 → if ( 𝜓 , 𝐴 , 𝐵 ) = 𝐶 )