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

Metamath Proof Explorer

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 ) )