Metamath Proof Explorer


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 φ θ
Assertion 3biant1d φ χ ψ θ χ ψ

Proof

Step Hyp Ref Expression
1 3biantd.1 φ θ
2 1 biantrurd φ χ ψ θ χ ψ
3 3anass θ χ ψ θ χ ψ
4 2 3 bitr4di φ χ ψ θ χ ψ