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  3307  reuun2  3446  prel12  3801  exmid01  4231  exmidsssnc  4236  ordtriexmid  4557  ordtri2orexmid  4559  ontr2exmid  4561  onsucsssucexmid  4563  ordsoexmid  4598  ordtri2or2exmid  4607  cnvsom  5213  fununi  5326  frec0g  6455  frecabcl  6457  frecsuclem  6464  swoer  6620  inffiexmid  6967  exmidontriimlem1  7288  enq0tr  7501  letr  8109  reapmul1  8622  reapneg  8624  reapcotr  8625  remulext1  8626  apsym  8633  mulext1  8639  elznn0nn  9340  elznn0  9341  zapne  9400  nneoor  9428  nn01to3  9691  ltxr  9850  xrletr  9883  maxclpr  11387  minclpr  11402  odd2np1lem  12037  lcmcom  12232  dvdsprime  12290  coprm  12312  opprdomnbg  13830  bdbl  14739  cos11  15089  lgsdir2lem4  15272  subctctexmid  15645