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  2064  dvelimfv  2065  dvelimor  2072  eueq2dc  2990  uncom  3363  reuun2  3504  prel12  3875  exmid01  4311  exmidsssnc  4316  ordtriexmid  4643  ordtri2orexmid  4645  ontr2exmid  4647  onsucsssucexmid  4649  ordsoexmid  4684  ordtri2or2exmid  4693  cnvsom  5306  fununi  5424  frec0g  6628  frecabcl  6630  frecsuclem  6637  swoer  6795  inffiexmid  7166  exmidontriimlem1  7528  enq0tr  7749  letr  8356  reapmul1  8869  reapneg  8871  reapcotr  8872  remulext1  8873  apsym  8880  mulext1  8886  elznn0nn  9591  elznn0  9592  zapne  9652  nneoor  9680  nn01to3  9949  ltxr  10108  xrletr  10141  swrdnd  11351  maxclpr  11907  minclpr  11922  odd2np1lem  12558  lcmcom  12761  dvdsprime  12819  coprm  12841  opprdomnbg  14420  bdbl  15368  cos11  15718  lgsdir2lem4  15904  vtxd0nedgbfi  16294  eupth2lem2dc  16454  eupth2lem3lem6fi  16466  subctctexmid  16774