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

Theorem orass 917
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 866 . 2 (((𝜑𝜓) ∨ 𝜒) ↔ (𝜒 ∨ (𝜑𝜓)))
2 or12 916 . 2 ((𝜒 ∨ (𝜑𝜓)) ↔ (𝜑 ∨ (𝜒𝜓)))
3 orcom 866 . . 3 ((𝜒𝜓) ↔ (𝜓𝜒))
43orbi2i 908 . 2 ((𝜑 ∨ (𝜒𝜓)) ↔ (𝜑 ∨ (𝜓𝜒)))
51, 2, 43bitri 298 1 (((𝜑𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wb 207  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 208  df-or 844
This theorem is referenced by:  pm2.31  918  pm2.32  919  or32  921  or4  922  3orass  1084  axi12  2794  axi12OLD  2795  axbnd  2796  unass  4146  tppreqb  4737  ltxr  12500  lcmass  15948  plydivex  24801  clwwlkneq0  27721  disjxpin  30253  impor  35227  ifpim123g  39731
  Copyright terms: Public domain W3C validator