Theorem orcom 718

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

Syntax hints:   <-> wb 104   \/ wo 698

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  orcomd  719  orbi1i  753  orass  757  or32  760  or42  762  orbi1d  781  pm5.61  784  oranabs  805  ordir  807  pm2.1dc  823  notnotrdc  829  dcnnOLD  835  pm5.17dc  890  pm5.7dc  939  dn1dc  945  pm5.75  947  3orrot  969  3orcomb  972  excxor  1357  xorcom  1367  19.33b2  1609  nf4dc  1649  nf4r  1650  19.31r  1660  dveeq2  1788  sbequilem  1811  dvelimALT  1986  dvelimfv  1987  dvelimor  1994  eueq2dc  2861  uncom  3225  reuun2  3364  prel12  3706  exmid01  4129  exmidsssnc  4134  ordtriexmid  4445  ordtri2orexmid  4446  ontr2exmid  4448  onsucsssucexmid  4450  ordsoexmid  4485  ordtri2or2exmid  4494  cnvsom  5090  fununi  5199  frec0g  6302  frecabcl  6304  frecsuclem  6311  swoer  6465  inffiexmid  6808  enq0tr  7266  letr  7871  reapmul1  8381  reapneg  8383  reapcotr  8384  remulext1  8385  apsym  8392  mulext1  8398  elznn0nn  9092  elznn0  9093  zapne  9149  nneoor  9177  nn01to3  9436  ltxr  9592  xrletr  9621  maxclpr  11026  minclpr  11040  odd2np1lem  11605  lcmcom  11781  dvdsprime  11839  coprm  11858  bdbl  12711  cos11  12982  subctctexmid  13369