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  6563  frecabcl  6565  frecsuclem  6572  swoer  6730  inffiexmid  7098  exmidontriimlem1  7436  enq0tr  7654  letr  8262  reapmul1  8775  reapneg  8777  reapcotr  8778  remulext1  8779  apsym  8786  mulext1  8792  elznn0nn  9493  elznn0  9494  zapne  9554  nneoor  9582  nn01to3  9851  ltxr  10010  xrletr  10043  swrdnd  11244  maxclpr  11800  minclpr  11815  odd2np1lem  12451  lcmcom  12654  dvdsprime  12712  coprm  12734  opprdomnbg  14307  bdbl  15246  cos11  15596  lgsdir2lem4  15779  vtxd0nedgbfi  16169  eupth2lem2dc  16329  eupth2lem3lem6fi  16341  subctctexmid  16652