Theorem orcom 729

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	⊢ ((𝜑 ∨ 𝜓) ↔ (𝜓 ∨ 𝜑))

Proof of Theorem orcom

Step	Hyp	Ref	Expression
1		pm1.4 728	. 2 ⊢ ((𝜑 ∨ 𝜓) → (𝜓 ∨ 𝜑))
2		pm1.4 728	. 2 ⊢ ((𝜓 ∨ 𝜑) → (𝜑 ∨ 𝜓))
3	1, 2	impbii 126	1 ⊢ ((𝜑 ∨ 𝜓) ↔ (𝜓 ∨ 𝜑))

Syntax hints:   ↔ wb 105   ∨ wo 709

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 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orcomd  730  orbi1i  764  orass  768  or32  771  or42  773  orbi1d  792  pm5.61  795  oranabs  816  ordir  818  pm2.1dc  838  notnotrdc  844  dcnnOLD  850  pm5.17dc  905  pm5.7dc  956  dn1dc  962  pm5.75  964  3orrot  986  3orcomb  989  excxor  1389  xorcom  1399  19.33b2  1640  nf4dc  1681  nf4r  1682  19.31r  1692  dveeq2  1826  sbequilem  1849  dvelimALT  2026  dvelimfv  2027  dvelimor  2034  eueq2dc  2933  uncom  3303  reuun2  3442  prel12  3797  exmid01  4227  exmidsssnc  4232  ordtriexmid  4553  ordtri2orexmid  4555  ontr2exmid  4557  onsucsssucexmid  4559  ordsoexmid  4594  ordtri2or2exmid  4603  cnvsom  5209  fununi  5322  frec0g  6450  frecabcl  6452  frecsuclem  6459  swoer  6615  inffiexmid  6962  exmidontriimlem1  7281  enq0tr  7494  letr  8102  reapmul1  8614  reapneg  8616  reapcotr  8617  remulext1  8618  apsym  8625  mulext1  8631  elznn0nn  9331  elznn0  9332  zapne  9391  nneoor  9419  nn01to3  9682  ltxr  9841  xrletr  9874  maxclpr  11366  minclpr  11380  odd2np1lem  12013  lcmcom  12202  dvdsprime  12260  coprm  12282  opprdomnbg  13770  bdbl  14671  cos11  14988  lgsdir2lem4  15147  subctctexmid  15491