Theorem orcom 718

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

Syntax hints:   <-> wb 104   \/ wo 698

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  orcomd  719  orbi1i  753  orass  757  or32  760  or42  762  orbi1d  781  pm5.61  784  oranabs  805  ordir  807  pm2.1dc  823  notnotrdc  829  dcnnOLD  835  pm5.17dc  890  pm5.7dc  939  dn1dc  945  pm5.75  947  3orrot  969  3orcomb  972  excxor  1360  xorcom  1370  19.33b2  1609  nf4dc  1650  nf4r  1651  19.31r  1661  dveeq2  1795  sbequilem  1818  dvelimALT  1990  dvelimfv  1991  dvelimor  1998  eueq2dc  2885  uncom  3251  reuun2  3390  prel12  3734  exmid01  4159  exmidsssnc  4164  ordtriexmid  4480  ordtri2orexmid  4482  ontr2exmid  4484  onsucsssucexmid  4486  ordsoexmid  4521  ordtri2or2exmid  4530  cnvsom  5129  fununi  5238  frec0g  6344  frecabcl  6346  frecsuclem  6353  swoer  6508  inffiexmid  6851  exmidontriimlem1  7156  enq0tr  7354  letr  7960  reapmul1  8470  reapneg  8472  reapcotr  8473  remulext1  8474  apsym  8481  mulext1  8487  elznn0nn  9181  elznn0  9182  zapne  9238  nneoor  9266  nn01to3  9526  ltxr  9682  xrletr  9712  maxclpr  11122  minclpr  11136  odd2np1lem  11762  lcmcom  11940  dvdsprime  11998  coprm  12018  bdbl  12903  cos11  13174  subctctexmid  13573