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  1643  nf4dc  1684  nf4r  1685  19.31r  1695  dveeq2  1829  sbequilem  1852  dvelimALT  2029  dvelimfv  2030  dvelimor  2037  eueq2dc  2937  uncom  3308  reuun2  3447  prel12  3802  exmid01  4232  exmidsssnc  4237  ordtriexmid  4558  ordtri2orexmid  4560  ontr2exmid  4562  onsucsssucexmid  4564  ordsoexmid  4599  ordtri2or2exmid  4608  cnvsom  5214  fununi  5327  frec0g  6464  frecabcl  6466  frecsuclem  6473  swoer  6629  inffiexmid  6976  exmidontriimlem1  7306  enq0tr  7520  letr  8128  reapmul1  8641  reapneg  8643  reapcotr  8644  remulext1  8645  apsym  8652  mulext1  8658  elznn0nn  9359  elznn0  9360  zapne  9419  nneoor  9447  nn01to3  9710  ltxr  9869  xrletr  9902  maxclpr  11406  minclpr  11421  odd2np1lem  12056  lcmcom  12259  dvdsprime  12317  coprm  12339  opprdomnbg  13908  bdbl  14847  cos11  15197  lgsdir2lem4  15380  subctctexmid  15755