Theorem 3biant1d

Description: A conjunction is equivalent to a threefold conjunction with single truth, analogous to biantrud . (Contributed by Alexander van der Vekens, 26-Sep-2017)

	Ref	Expression
Hypothesis	3biantd.1	|- ( ph -> th )
Assertion	3biant1d	|- ( ph -> ( ( ch /\ ps ) <-> ( th /\ ch /\ ps ) ) )

Proof

Step	Hyp	Ref	Expression
1		3biantd.1	|- ( ph -> th )
2	1	biantrurd	|- ( ph -> ( ( ch /\ ps ) <-> ( th /\ ( ch /\ ps ) ) ) )
3		3anass	|- ( ( th /\ ch /\ ps ) <-> ( th /\ ( ch /\ ps ) ) )
4	2 3	bitr4di	|- ( ph -> ( ( ch /\ ps ) <-> ( th /\ ch /\ ps ) ) )