Theorem orcom 728

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 727	. 2 ⊢ ((𝜑 ∨ 𝜓) → (𝜓 ∨ 𝜑))
2		pm1.4 727	. 2 ⊢ ((𝜓 ∨ 𝜑) → (𝜑 ∨ 𝜓))
3	1, 2	impbii 126	1 ⊢ ((𝜑 ∨ 𝜓) ↔ (𝜓 ∨ 𝜑))

Syntax hints:   ↔ wb 105   ∨ wo 708

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 709

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orcomd  729  orbi1i  763  orass  767  or32  770  or42  772  orbi1d  791  pm5.61  794  oranabs  815  ordir  817  pm2.1dc  837  notnotrdc  843  dcnnOLD  849  pm5.17dc  904  pm5.7dc  954  dn1dc  960  pm5.75  962  3orrot  984  3orcomb  987  excxor  1378  xorcom  1388  19.33b2  1629  nf4dc  1670  nf4r  1671  19.31r  1681  dveeq2  1815  sbequilem  1838  dvelimALT  2010  dvelimfv  2011  dvelimor  2018  eueq2dc  2911  uncom  3280  reuun2  3419  prel12  3772  exmid01  4199  exmidsssnc  4204  ordtriexmid  4521  ordtri2orexmid  4523  ontr2exmid  4525  onsucsssucexmid  4527  ordsoexmid  4562  ordtri2or2exmid  4571  cnvsom  5173  fununi  5285  frec0g  6398  frecabcl  6400  frecsuclem  6407  swoer  6563  inffiexmid  6906  exmidontriimlem1  7220  enq0tr  7433  letr  8040  reapmul1  8552  reapneg  8554  reapcotr  8555  remulext1  8556  apsym  8563  mulext1  8569  elznn0nn  9267  elznn0  9268  zapne  9327  nneoor  9355  nn01to3  9617  ltxr  9775  xrletr  9808  maxclpr  11231  minclpr  11245  odd2np1lem  11877  lcmcom  12064  dvdsprime  12122  coprm  12144  bdbl  14006  cos11  14277  lgsdir2lem4  14435  subctctexmid  14753