Theorem orcom 646

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 645	. 2 ⊢ ((φ ∨ ψ) → (ψ ∨ φ))
2		pm1.4 645	. 2 ⊢ ((ψ ∨ φ) → (φ ∨ ψ))
3	1, 2	impbii 117	1 ⊢ ((φ ∨ ψ) ↔ (ψ ∨ φ))

Syntax hints:   ↔ wb 98   ∨ wo 628

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  orcomd  647  orbi1i  679  orass  683  or32  686  or42  688  orbi1d  704  pm5.61  707  oranabs  727  ordir  729  pm2.1dc  744  notnot2dc  750  pm5.17dc  809  testbitestn  822  pm5.7dc  860  dn1dc  866  pm5.75  868  3orrot  890  3orcomb  893  excxor  1268  xorcom  1276  19.33b2  1517  nf4dc  1557  nf4r  1558  19.31r  1568  dveeq2  1693  sbequilem  1716  dvelimALT  1883  dvelimfv  1884  dvelimor  1891  eueq2dc  2708  uncom  3081  reuun2  3214  prel12  3533  ordtriexmid  4210  ordtri2orexmid  4211  onsucsssucexmid  4212  ordsoexmid  4240  cnvsom  4804  fununi  4910  frec0g  5922  frecsuclem3  5929  swoer  6070  enq0tr  6416  letr  6858  reapmul1  7339  reapneg  7341  reapcotr  7342  remulext1  7343  apsym  7350  mulext1  7356  elznn0nn  7995  elznn0  7996  zapne  8051  nneoor  8076  nn01to3  8288  ltxr  8425  xrletr  8454