Theorem 3r19.43

Description: Restricted quantifier version of 19.43 for a triple disjunction . (Contributed by AV, 2-Nov-2025)

	Ref	Expression
Assertion	3r19.43	|- ( E. x e. A ( ph \/ ps \/ ch ) <-> ( E. x e. A ph \/ E. x e. A ps \/ E. x e. A ch ) )

Proof

Step	Hyp	Ref	Expression
1		df-3or	|- ( ( ph \/ ps \/ ch ) <-> ( ( ph \/ ps ) \/ ch ) )
2	1	rexbii	|- ( E. x e. A ( ph \/ ps \/ ch ) <-> E. x e. A ( ( ph \/ ps ) \/ ch ) )
3		r19.43	|- ( E. x e. A ( ( ph \/ ps ) \/ ch ) <-> ( E. x e. A ( ph \/ ps ) \/ E. x e. A ch ) )
4		r19.43	|- ( E. x e. A ( ph \/ ps ) <-> ( E. x e. A ph \/ E. x e. A ps ) )
5	4	orbi1i	|- ( ( E. x e. A ( ph \/ ps ) \/ E. x e. A ch ) <-> ( ( E. x e. A ph \/ E. x e. A ps ) \/ E. x e. A ch ) )
6		df-3or	|- ( ( E. x e. A ph \/ E. x e. A ps \/ E. x e. A ch ) <-> ( ( E. x e. A ph \/ E. x e. A ps ) \/ E. x e. A ch ) )
7	5 6	bitr4i	|- ( ( E. x e. A ( ph \/ ps ) \/ E. x e. A ch ) <-> ( E. x e. A ph \/ E. x e. A ps \/ E. x e. A ch ) )
8	2 3 7	3bitri	|- ( E. x e. A ( ph \/ ps \/ ch ) <-> ( E. x e. A ph \/ E. x e. A ps \/ E. x e. A ch ) )