Metamath Proof Explorer


Theorem or4

Description: Rearrangement of 4 disjuncts. (Contributed by NM, 12-Aug-1994)

Ref Expression
Assertion or4 ( ( ( 𝜑𝜓 ) ∨ ( 𝜒𝜃 ) ) ↔ ( ( 𝜑𝜒 ) ∨ ( 𝜓𝜃 ) ) )

Proof

Step Hyp Ref Expression
1 or12 ( ( 𝜓 ∨ ( 𝜒𝜃 ) ) ↔ ( 𝜒 ∨ ( 𝜓𝜃 ) ) )
2 1 orbi2i ( ( 𝜑 ∨ ( 𝜓 ∨ ( 𝜒𝜃 ) ) ) ↔ ( 𝜑 ∨ ( 𝜒 ∨ ( 𝜓𝜃 ) ) ) )
3 orass ( ( ( 𝜑𝜓 ) ∨ ( 𝜒𝜃 ) ) ↔ ( 𝜑 ∨ ( 𝜓 ∨ ( 𝜒𝜃 ) ) ) )
4 orass ( ( ( 𝜑𝜒 ) ∨ ( 𝜓𝜃 ) ) ↔ ( 𝜑 ∨ ( 𝜒 ∨ ( 𝜓𝜃 ) ) ) )
5 2 3 4 3bitr4i ( ( ( 𝜑𝜓 ) ∨ ( 𝜒𝜃 ) ) ↔ ( ( 𝜑𝜒 ) ∨ ( 𝜓𝜃 ) ) )