Metamath Proof Explorer


Theorem or42

Description: Rearrangement of 4 disjuncts. (Contributed by NM, 10-Jan-2005)

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

Proof

Step Hyp Ref Expression
1 or4 ( ( ( 𝜑𝜓 ) ∨ ( 𝜒𝜃 ) ) ↔ ( ( 𝜑𝜒 ) ∨ ( 𝜓𝜃 ) ) )
2 orcom ( ( 𝜓𝜃 ) ↔ ( 𝜃𝜓 ) )
3 2 orbi2i ( ( ( 𝜑𝜒 ) ∨ ( 𝜓𝜃 ) ) ↔ ( ( 𝜑𝜒 ) ∨ ( 𝜃𝜓 ) ) )
4 1 3 bitri ( ( ( 𝜑𝜓 ) ∨ ( 𝜒𝜃 ) ) ↔ ( ( 𝜑𝜒 ) ∨ ( 𝜃𝜓 ) ) )