Metamath Proof Explorer


Theorem anandir

Description: Distribution of conjunction over conjunction. (Contributed by NM, 24-Aug-1995)

Ref Expression
Assertion anandir ( ( ( 𝜑𝜓 ) ∧ 𝜒 ) ↔ ( ( 𝜑𝜒 ) ∧ ( 𝜓𝜒 ) ) )

Proof

Step Hyp Ref Expression
1 anidm ( ( 𝜒𝜒 ) ↔ 𝜒 )
2 1 anbi2i ( ( ( 𝜑𝜓 ) ∧ ( 𝜒𝜒 ) ) ↔ ( ( 𝜑𝜓 ) ∧ 𝜒 ) )
3 an4 ( ( ( 𝜑𝜓 ) ∧ ( 𝜒𝜒 ) ) ↔ ( ( 𝜑𝜒 ) ∧ ( 𝜓𝜒 ) ) )
4 2 3 bitr3i ( ( ( 𝜑𝜓 ) ∧ 𝜒 ) ↔ ( ( 𝜑𝜒 ) ∧ ( 𝜓𝜒 ) ) )