Theorem orcom 736

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

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

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 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orcomd  737  orbi1i  771  orass  775  or32  778  or42  780  orbi1d  799  pm5.61  802  oranabs  823  ordir  825  pm2.1dc  845  notnotrdc  851  dcnnOLD  857  pm5.17dc  912  pm5.7dc  963  dn1dc  969  pm5.75  971  3orrot  1011  3orcomb  1014  excxor  1423  xorcom  1433  19.33b2  1678  nf4dc  1718  nf4r  1719  19.31r  1729  dveeq2  1864  sbequilem  1887  dvelimALT  2066  dvelimfv  2067  dvelimor  2074  eueq2dc  2992  uncom  3365  reuun2  3506  prel12  3877  exmid01  4313  exmidsssnc  4318  ordtriexmid  4645  ordtri2orexmid  4647  ontr2exmid  4649  onsucsssucexmid  4651  ordsoexmid  4686  ordtri2or2exmid  4695  cnvsom  5308  fununi  5426  frec0g  6630  frecabcl  6632  frecsuclem  6639  swoer  6797  inffiexmid  7168  exmidontriimlem1  7530  enq0tr  7751  letr  8358  reapmul1  8871  reapneg  8873  reapcotr  8874  remulext1  8875  apsym  8882  mulext1  8888  elznn0nn  9593  elznn0  9594  zapne  9654  nneoor  9683  nn01to3  9952  ltxr  10111  xrletr  10144  swrdnd  11355  maxclpr  11911  minclpr  11926  odd2np1lem  12562  lcmcom  12765  dvdsprime  12823  coprm  12845  ballotfilemfc0  13153  ballotfilemfcc  13154  opprdomnbg  14437  bdbl  15385  cos11  15735  lgsdir2lem4  15921  vtxd0nedgbfi  16311  eupth2lem2dc  16471  eupth2lem3lem6fi  16483  subctctexmid  16791