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 -> ph )
	jaeqifi.2	|- ( A = D -> ph )
	jaeqifi.3	|- ( B = C -> ph )
	jaeqifi.4	|- ( B = D -> ph )
Assertion	jaeqifi	|- ( if ( ps , A , B ) = if ( ch , C , D ) -> ph )

Proof

Step	Hyp	Ref	Expression
1		jaeqifi.1	|- ( A = C -> ph )
2		jaeqifi.2	|- ( A = D -> ph )
3		jaeqifi.3	|- ( B = C -> ph )
4		jaeqifi.4	|- ( B = D -> ph )
5		iftrue	|- ( ps -> if ( ps , A , B ) = A )
6		iftrue	|- ( ch -> if ( ch , C , D ) = C )
7	5 6	eqeqan12d	|- ( ( ps /\ ch ) -> ( if ( ps , A , B ) = if ( ch , C , D ) <-> A = C ) )
8	7 1	biimtrdi	|- ( ( ps /\ ch ) -> ( if ( ps , A , B ) = if ( ch , C , D ) -> ph ) )
9		iffalse	|- ( -. ch -> if ( ch , C , D ) = D )
10	5 9	eqeqan12d	|- ( ( ps /\ -. ch ) -> ( if ( ps , A , B ) = if ( ch , C , D ) <-> A = D ) )
11	10 2	biimtrdi	|- ( ( ps /\ -. ch ) -> ( if ( ps , A , B ) = if ( ch , C , D ) -> ph ) )
12		iffalse	|- ( -. ps -> if ( ps , A , B ) = B )
13	12 6	eqeqan12d	|- ( ( -. ps /\ ch ) -> ( if ( ps , A , B ) = if ( ch , C , D ) <-> B = C ) )
14	13 3	biimtrdi	|- ( ( -. ps /\ ch ) -> ( if ( ps , A , B ) = if ( ch , C , D ) -> ph ) )
15	12 9	eqeqan12d	|- ( ( -. ps /\ -. ch ) -> ( if ( ps , A , B ) = if ( ch , C , D ) <-> B = D ) )
16	15 4	biimtrdi	|- ( ( -. ps /\ -. ch ) -> ( if ( ps , A , B ) = if ( ch , C , D ) -> ph ) )
17	8 11 14 16	4cases	|- ( if ( ps , A , B ) = if ( ch , C , D ) -> ph )