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  1652  nf4dc  1693  nf4r  1694  19.31r  1704  dveeq2  1838  sbequilem  1861  dvelimALT  2038  dvelimfv  2039  dvelimor  2046  eueq2dc  2946  uncom  3317  reuun2  3456  prel12  3812  exmid01  4242  exmidsssnc  4247  ordtriexmid  4569  ordtri2orexmid  4571  ontr2exmid  4573  onsucsssucexmid  4575  ordsoexmid  4610  ordtri2or2exmid  4619  cnvsom  5226  fununi  5342  frec0g  6483  frecabcl  6485  frecsuclem  6492  swoer  6648  inffiexmid  7003  exmidontriimlem1  7333  enq0tr  7547  letr  8155  reapmul1  8668  reapneg  8670  reapcotr  8671  remulext1  8672  apsym  8679  mulext1  8685  elznn0nn  9386  elznn0  9387  zapne  9447  nneoor  9475  nn01to3  9738  ltxr  9897  xrletr  9930  swrdnd  11112  maxclpr  11533  minclpr  11548  odd2np1lem  12183  lcmcom  12386  dvdsprime  12444  coprm  12466  opprdomnbg  14036  bdbl  14975  cos11  15325  lgsdir2lem4  15508  subctctexmid  15937