Theorem orcom 679

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

Syntax hints:   <-> wb 103   \/ wo 661

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  orcomd  680  orbi1i  712  orass  716  or32  719  or42  721  orbi1d  737  pm5.61  740  oranabs  761  ordir  763  pm2.1dc  778  notnotrdc  784  pm5.17dc  843  testbitestn  856  pm5.7dc  895  dn1dc  901  pm5.75  903  3orrot  925  3orcomb  928  excxor  1309  xorcom  1319  19.33b2  1560  nf4dc  1600  nf4r  1601  19.31r  1611  dveeq2  1736  sbequilem  1759  dvelimALT  1927  dvelimfv  1928  dvelimor  1935  eueq2dc  2765  uncom  3116  reuun2  3247  prel12  3563  ordtriexmid  4265  ordtri2orexmid  4266  ontr2exmid  4268  onsucsssucexmid  4270  ordsoexmid  4305  ordtri2or2exmid  4314  cnvsom  4881  fununi  4987  frec0g  6006  frecsuclem3  6013  swoer  6157  enq0tr  6624  letr  7194  reapmul1  7695  reapneg  7697  reapcotr  7698  remulext1  7699  apsym  7706  mulext1  7712  elznn0nn  8365  elznn0  8366  zapne  8422  nneoor  8449  nn01to3  8702  ltxr  8849  xrletr  8878  maxclpr  10108  odd2np1lem  10271  lcmcom  10446  dvdsprime  10504  coprm  10523