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 ( 𝜑 → ( ( 𝜒𝜓 ) ↔ ( 𝜃𝜒𝜓 ) ) )