This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem or3di

Description: Distributive law for disjunction. (Contributed by Thierry Arnoux, 3-Jul-2017)

Ref Expression
Assertion or3di ( ( 𝜑 ∨ ( 𝜓 ∧ 𝜒 ∧ 𝜏 ) ) ↔ ( ( 𝜑 ∨ 𝜓 ) ∧ ( 𝜑 ∨ 𝜒 ) ∧ ( 𝜑 ∨ 𝜏 ) ) )

Proof

Step Hyp Ref Expression
1 df-3an ⊢ ( ( 𝜓 ∧ 𝜒 ∧ 𝜏 ) ↔ ( ( 𝜓 ∧ 𝜒 ) ∧ 𝜏 ) )
2 1 orbi2i ⊢ ( ( 𝜑 ∨ ( 𝜓 ∧ 𝜒 ∧ 𝜏 ) ) ↔ ( 𝜑 ∨ ( ( 𝜓 ∧ 𝜒 ) ∧ 𝜏 ) ) )
3 ordi ⊢ ( ( 𝜑 ∨ ( ( 𝜓 ∧ 𝜒 ) ∧ 𝜏 ) ) ↔ ( ( 𝜑 ∨ ( 𝜓 ∧ 𝜒 ) ) ∧ ( 𝜑 ∨ 𝜏 ) ) )
4 ordi ⊢ ( ( 𝜑 ∨ ( 𝜓 ∧ 𝜒 ) ) ↔ ( ( 𝜑 ∨ 𝜓 ) ∧ ( 𝜑 ∨ 𝜒 ) ) )
5 4 anbi1i ⊢ ( ( ( 𝜑 ∨ ( 𝜓 ∧ 𝜒 ) ) ∧ ( 𝜑 ∨ 𝜏 ) ) ↔ ( ( ( 𝜑 ∨ 𝜓 ) ∧ ( 𝜑 ∨ 𝜒 ) ) ∧ ( 𝜑 ∨ 𝜏 ) ) )
6 2 3 5 3bitri ⊢ ( ( 𝜑 ∨ ( 𝜓 ∧ 𝜒 ∧ 𝜏 ) ) ↔ ( ( ( 𝜑 ∨ 𝜓 ) ∧ ( 𝜑 ∨ 𝜒 ) ) ∧ ( 𝜑 ∨ 𝜏 ) ) )
7 df-3an ⊢ ( ( ( 𝜑 ∨ 𝜓 ) ∧ ( 𝜑 ∨ 𝜒 ) ∧ ( 𝜑 ∨ 𝜏 ) ) ↔ ( ( ( 𝜑 ∨ 𝜓 ) ∧ ( 𝜑 ∨ 𝜒 ) ) ∧ ( 𝜑 ∨ 𝜏 ) ) )
8 6 7 bitr4i ⊢ ( ( 𝜑 ∨ ( 𝜓 ∧ 𝜒 ∧ 𝜏 ) ) ↔ ( ( 𝜑 ∨ 𝜓 ) ∧ ( 𝜑 ∨ 𝜒 ) ∧ ( 𝜑 ∨ 𝜏 ) ) )