Description: Split a biconditional and distribute two restricted universal quantifiers, analogous to 2albiim and ralbiim . (Contributed by Alexander van der Vekens, 2-Jul-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | 2ralbiim |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralbiim | ||
2 | 1 | ralbii | |
3 | r19.26 | ||
4 | 2 3 | bitri |