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  2912  uncom  3281  reuun2  3420  prel12  3773  exmid01  4200  exmidsssnc  4205  ordtriexmid  4522  ordtri2orexmid  4524  ontr2exmid  4526  onsucsssucexmid  4528  ordsoexmid  4563  ordtri2or2exmid  4572  cnvsom  5174  fununi  5286  frec0g  6400  frecabcl  6402  frecsuclem  6409  swoer  6565  inffiexmid  6908  exmidontriimlem1  7222  enq0tr  7435  letr  8042  reapmul1  8554  reapneg  8556  reapcotr  8557  remulext1  8558  apsym  8565  mulext1  8571  elznn0nn  9269  elznn0  9270  zapne  9329  nneoor  9357  nn01to3  9619  ltxr  9777  xrletr  9810  maxclpr  11233  minclpr  11247  odd2np1lem  11879  lcmcom  12066  dvdsprime  12124  coprm  12146  bdbl  14088  cos11  14359  lgsdir2lem4  14517  subctctexmid  14835