Theorem orcom 730

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 729	. 2 |- ( ( ph \/ ps ) -> ( ps \/ ph ) )
2		pm1.4 729	. 2 |- ( ( ps \/ ph ) -> ( ph \/ ps ) )
3	1, 2	impbii 126	1 |- ( ( ph \/ ps ) <-> ( ps \/ ph ) )

Syntax hints:   <-> wb 105   \/ wo 710

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orcomd  731  orbi1i  765  orass  769  or32  772  or42  774  orbi1d  793  pm5.61  796  oranabs  817  ordir  819  pm2.1dc  839  notnotrdc  845  dcnnOLD  851  pm5.17dc  906  pm5.7dc  957  dn1dc  963  pm5.75  965  3orrot  987  3orcomb  990  excxor  1398  xorcom  1408  19.33b2  1653  nf4dc  1694  nf4r  1695  19.31r  1705  dveeq2  1839  sbequilem  1862  dvelimALT  2039  dvelimfv  2040  dvelimor  2047  eueq2dc  2953  uncom  3325  reuun2  3464  prel12  3825  exmid01  4258  exmidsssnc  4263  ordtriexmid  4587  ordtri2orexmid  4589  ontr2exmid  4591  onsucsssucexmid  4593  ordsoexmid  4628  ordtri2or2exmid  4637  cnvsom  5245  fununi  5361  frec0g  6506  frecabcl  6508  frecsuclem  6515  swoer  6671  inffiexmid  7029  exmidontriimlem1  7364  enq0tr  7582  letr  8190  reapmul1  8703  reapneg  8705  reapcotr  8706  remulext1  8707  apsym  8714  mulext1  8720  elznn0nn  9421  elznn0  9422  zapne  9482  nneoor  9510  nn01to3  9773  ltxr  9932  xrletr  9965  swrdnd  11150  maxclpr  11648  minclpr  11663  odd2np1lem  12298  lcmcom  12501  dvdsprime  12559  coprm  12581  opprdomnbg  14151  bdbl  15090  cos11  15440  lgsdir2lem4  15623  subctctexmid  16139