Theorem orass 918

Description: Associative law for disjunction. Theorem *4.33 of [WhiteheadRussell] p. 118. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)

Assertion

Ref	Expression
orass	⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))

Proof of Theorem orass

Step	Hyp	Ref	Expression
1		orcom 866	. 2 ⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜒 ∨ (𝜑 ∨ 𝜓)))
2		or12 917	. 2 ⊢ ((𝜒 ∨ (𝜑 ∨ 𝜓)) ↔ (𝜑 ∨ (𝜒 ∨ 𝜓)))
3		orcom 866	. . 3 ⊢ ((𝜒 ∨ 𝜓) ↔ (𝜓 ∨ 𝜒))
4	3	orbi2i 909	. 2 ⊢ ((𝜑 ∨ (𝜒 ∨ 𝜓)) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))
5	1, 2, 4	3bitri 299	1 ⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))

Syntax hints:   ↔ wb 208   ∨ wo 843

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209  df-or 844

This theorem is referenced by:  pm2.31  919  pm2.32  920  or32  922  or4  923  3orass  1085  axi12  2787  axi12OLD  2788  axbnd  2789  unass  4140  tppreqb  4730  ltxr  12502  lcmass  15950  plydivex  24878  clwwlkneq0  27799  disjxpin  30330  impor  35351  ifpim123g  39856