Theorem orcom 728

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

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

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 709

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orcomd  729  orbi1i  763  orass  767  or32  770  or42  772  orbi1d  791  pm5.61  794  oranabs  815  ordir  817  pm2.1dc  837  notnotrdc  843  dcnnOLD  849  pm5.17dc  904  pm5.7dc  954  dn1dc  960  pm5.75  962  3orrot  984  3orcomb  987  excxor  1378  xorcom  1388  19.33b2  1629  nf4dc  1670  nf4r  1671  19.31r  1681  dveeq2  1815  sbequilem  1838  dvelimALT  2010  dvelimfv  2011  dvelimor  2018  eueq2dc  2910  uncom  3279  reuun2  3418  prel12  3771  exmid01  4198  exmidsssnc  4203  ordtriexmid  4520  ordtri2orexmid  4522  ontr2exmid  4524  onsucsssucexmid  4526  ordsoexmid  4561  ordtri2or2exmid  4570  cnvsom  5172  fununi  5284  frec0g  6397  frecabcl  6399  frecsuclem  6406  swoer  6562  inffiexmid  6905  exmidontriimlem1  7219  enq0tr  7432  letr  8038  reapmul1  8550  reapneg  8552  reapcotr  8553  remulext1  8554  apsym  8561  mulext1  8567  elznn0nn  9265  elznn0  9266  zapne  9325  nneoor  9353  nn01to3  9615  ltxr  9773  xrletr  9806  maxclpr  11226  minclpr  11240  odd2np1lem  11871  lcmcom  12058  dvdsprime  12116  coprm  12138  bdbl  13896  cos11  14167  lgsdir2lem4  14325  subctctexmid  14632