Theorem orcom 376

Description: Commutative law for disjunction. Theorem *4.31 of [WhiteheadRussell] p. 118. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 15-Nov-2012.)

Assertion

Ref	Expression
orcom	|- ((ph \/ ps) <-> (ps \/ ph))

Proof of Theorem orcom

Step	Hyp	Ref	Expression
1		pm1.4 375	. 2 |- ((ph \/ ps) -> (ps \/ ph))
2		pm1.4 375	. 2 |- ((ps \/ ph) -> (ph \/ ps))
3	1, 2	impbii 180	1 |- ((ph \/ ps) <-> (ps \/ ph))

Syntax hints:   <-> wb 176   \/ wo 357

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 177  df-or 359

This theorem is referenced by:  orcomd  377  orbi1i  506  orass  510  or32  513  or42  515  orbi1d  683  pm5.61  693  oranabs  829  ordir  835  pm5.17  858  pm5.7  900  pm5.75  903  dn1  932  3orrot  940  3orcomb  944  cadan  1392  nf4  1868  19.31  1876  r19.30  2757  eueq2  3011  uncom  3409  reuun2  3539  dfif2  3665  ssunsn2  3866  ltfintri  4467  evenoddnnnul  4515  dfphi2  4570  proj2op  4602  fununi  5161  fce  6189