Description: Join 3 biconditionals with conjunction. (Contributed by NM, 21-Apr-1994)
Ref | Expression | ||
---|---|---|---|
Hypotheses | bi3.1 | ||
bi3.2 | |||
bi3.3 | |||
Assertion | 3anbi123i |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bi3.1 | ||
2 | bi3.2 | ||
3 | bi3.3 | ||
4 | 1 2 | anbi12i | |
5 | 4 3 | anbi12i | |
6 | df-3an | ||
7 | df-3an | ||
8 | 5 6 7 | 3bitr4i |