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  1863  sbequilem  1886  dvelimALT  2063  dvelimfv  2064  dvelimor  2071  eueq2dc  2980  uncom  3353  reuun2  3492  prel12  3859  exmid01  4294  exmidsssnc  4299  ordtriexmid  4625  ordtri2orexmid  4627  ontr2exmid  4629  onsucsssucexmid  4631  ordsoexmid  4666  ordtri2or2exmid  4675  cnvsom  5287  fununi  5405  frec0g  6606  frecabcl  6608  frecsuclem  6615  swoer  6773  inffiexmid  7141  exmidontriimlem1  7479  enq0tr  7697  letr  8304  reapmul1  8817  reapneg  8819  reapcotr  8820  remulext1  8821  apsym  8828  mulext1  8834  elznn0nn  9537  elznn0  9538  zapne  9598  nneoor  9626  nn01to3  9895  ltxr  10054  xrletr  10087  swrdnd  11289  maxclpr  11845  minclpr  11860  odd2np1lem  12496  lcmcom  12699  dvdsprime  12757  coprm  12779  opprdomnbg  14353  bdbl  15297  cos11  15647  lgsdir2lem4  15833  vtxd0nedgbfi  16223  eupth2lem2dc  16383  eupth2lem3lem6fi  16395  subctctexmid  16705