Metamath Proof Explorer

Theorem an3andi

Description: Distribution of conjunction over threefold conjunction. (Contributed by Thierry Arnoux, 8-Apr-2019)

Ref Expression
Assertion an3andi 
|- ( ( ph /\ ( ps /\ ch /\ th ) ) <-> ( ( ph /\ ps ) /\ ( ph /\ ch ) /\ ( ph /\ th ) ) )

Proof

Step Hyp Ref Expression
1 df-3an 
 |-  ( ( ps /\ ch /\ th ) <-> ( ( ps /\ ch ) /\ th ) )
2 1 anbi2i 
 |-  ( ( ph /\ ( ps /\ ch /\ th ) ) <-> ( ph /\ ( ( ps /\ ch ) /\ th ) ) )
3 anandi 
 |-  ( ( ph /\ ( ( ps /\ ch ) /\ th ) ) <-> ( ( ph /\ ( ps /\ ch ) ) /\ ( ph /\ th ) ) )
4 anandi 
 |-  ( ( ph /\ ( ps /\ ch ) ) <-> ( ( ph /\ ps ) /\ ( ph /\ ch ) ) )
5 4 anbi1i 
 |-  ( ( ( ph /\ ( ps /\ ch ) ) /\ ( ph /\ th ) ) <-> ( ( ( ph /\ ps ) /\ ( ph /\ ch ) ) /\ ( ph /\ th ) ) )
6 2 3 5 3bitri 
 |-  ( ( ph /\ ( ps /\ ch /\ th ) ) <-> ( ( ( ph /\ ps ) /\ ( ph /\ ch ) ) /\ ( ph /\ th ) ) )
7 df-3an 
 |-  ( ( ( ph /\ ps ) /\ ( ph /\ ch ) /\ ( ph /\ th ) ) <-> ( ( ( ph /\ ps ) /\ ( ph /\ ch ) ) /\ ( ph /\ th ) ) )
8 6 7 bitr4i 
 |-  ( ( ph /\ ( ps /\ ch /\ th ) ) <-> ( ( ph /\ ps ) /\ ( ph /\ ch ) /\ ( ph /\ th ) ) )