Theorem orcom 735

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

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

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 716

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orcomd  736  orbi1i  770  orass  774  or32  777  or42  779  orbi1d  798  pm5.61  801  oranabs  822  ordir  824  pm2.1dc  844  notnotrdc  850  dcnnOLD  856  pm5.17dc  911  pm5.7dc  962  dn1dc  968  pm5.75  970  3orrot  1010  3orcomb  1013  excxor  1422  xorcom  1432  19.33b2  1677  nf4dc  1718  nf4r  1719  19.31r  1729  dveeq2  1863  sbequilem  1886  dvelimALT  2063  dvelimfv  2064  dvelimor  2071  eueq2dc  2979  uncom  3351  reuun2  3490  prel12  3854  exmid01  4288  exmidsssnc  4293  ordtriexmid  4619  ordtri2orexmid  4621  ontr2exmid  4623  onsucsssucexmid  4625  ordsoexmid  4660  ordtri2or2exmid  4669  cnvsom  5280  fununi  5398  frec0g  6562  frecabcl  6564  frecsuclem  6571  swoer  6729  inffiexmid  7097  exmidontriimlem1  7435  enq0tr  7653  letr  8261  reapmul1  8774  reapneg  8776  reapcotr  8777  remulext1  8778  apsym  8785  mulext1  8791  elznn0nn  9492  elznn0  9493  zapne  9553  nneoor  9581  nn01to3  9850  ltxr  10009  xrletr  10042  swrdnd  11239  maxclpr  11782  minclpr  11797  odd2np1lem  12432  lcmcom  12635  dvdsprime  12693  coprm  12715  opprdomnbg  14287  bdbl  15226  cos11  15576  lgsdir2lem4  15759  vtxd0nedgbfi  16149  eupth2lem2dc  16309  subctctexmid  16601