MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  orass Structured version   Visualization version   GIF version

Theorem orass 547
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
StepHypRef Expression
1 orcom 401 . 2 (((𝜑𝜓) ∨ 𝜒) ↔ (𝜒 ∨ (𝜑𝜓)))
2 or12 546 . 2 ((𝜒 ∨ (𝜑𝜓)) ↔ (𝜑 ∨ (𝜒𝜓)))
3 orcom 401 . . 3 ((𝜒𝜓) ↔ (𝜓𝜒))
43orbi2i 542 . 2 ((𝜑 ∨ (𝜒𝜓)) ↔ (𝜑 ∨ (𝜓𝜒)))
51, 2, 43bitri 286 1 (((𝜑𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wo 382
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 197  df-or 384
This theorem is referenced by:  pm2.31  548  pm2.32  549  or32  550  or4  551  3orass  1075  axi12  2738  unass  3913  tppreqb  4481  ltxr  12162  lcmass  15549  plydivex  24271  clwwlkneq0  27177  disjxpin  29729  impor  34211  ifpim123g  38365
  Copyright terms: Public domain W3C validator