Theorem jaeqifi

Description: Inference combining four equality antecedents into one equality of conditional operators antecedent. (Contributed by BTernaryTau, 14-Jul-2026)

	Ref	Expression
Hypotheses	jaeqifi.1	$$⊢A=C\to \phi$$
	jaeqifi.2	$$⊢A=D\to \phi$$
	jaeqifi.3	$$⊢B=C\to \phi$$
	jaeqifi.4	$$⊢B=D\to \phi$$
Assertion	jaeqifi	$$⊢if\left(\psi ,A,B\right)=if\left(\chi ,C,D\right)\to \phi$$

Proof

Step	Hyp	Ref	Expression
1		jaeqifi.1	$$⊢A=C\to \phi$$
2		jaeqifi.2	$$⊢A=D\to \phi$$
3		jaeqifi.3	$$⊢B=C\to \phi$$
4		jaeqifi.4	$$⊢B=D\to \phi$$
5		iftrue	$$⊢\psi \to if\left(\psi ,A,B\right)=A$$
6		iftrue	$$⊢\chi \to if\left(\chi ,C,D\right)=C$$
7	5 6	eqeqan12d	$$⊢\left(\psi \wedge \chi \right)\to \left(if\left(\psi ,A,B\right)=if\left(\chi ,C,D\right)\leftrightarrow A=C\right)$$
8	7 1	biimtrdi	$$⊢\left(\psi \wedge \chi \right)\to \left(if\left(\psi ,A,B\right)=if\left(\chi ,C,D\right)\to \phi \right)$$
9		iffalse	$$⊢\neg \chi \to if\left(\chi ,C,D\right)=D$$
10	5 9	eqeqan12d	$$⊢\left(\psi \wedge \neg \chi \right)\to \left(if\left(\psi ,A,B\right)=if\left(\chi ,C,D\right)\leftrightarrow A=D\right)$$
11	10 2	biimtrdi	$$⊢\left(\psi \wedge \neg \chi \right)\to \left(if\left(\psi ,A,B\right)=if\left(\chi ,C,D\right)\to \phi \right)$$
12		iffalse	$$⊢\neg \psi \to if\left(\psi ,A,B\right)=B$$
13	12 6	eqeqan12d	$$⊢\left(\neg \psi \wedge \chi \right)\to \left(if\left(\psi ,A,B\right)=if\left(\chi ,C,D\right)\leftrightarrow B=C\right)$$
14	13 3	biimtrdi	$$⊢\left(\neg \psi \wedge \chi \right)\to \left(if\left(\psi ,A,B\right)=if\left(\chi ,C,D\right)\to \phi \right)$$
15	12 9	eqeqan12d	$$⊢\left(\neg \psi \wedge \neg \chi \right)\to \left(if\left(\psi ,A,B\right)=if\left(\chi ,C,D\right)\leftrightarrow B=D\right)$$
16	15 4	biimtrdi	$$⊢\left(\neg \psi \wedge \neg \chi \right)\to \left(if\left(\psi ,A,B\right)=if\left(\chi ,C,D\right)\to \phi \right)$$
17	8 11 14 16	4cases	$$⊢if\left(\psi ,A,B\right)=if\left(\chi ,C,D\right)\to \phi$$