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  6417  letr  6898  reapmul1  7379  reapneg  7381  reapcotr  7382  remulext1  7383  apsym  7390  mulext1  7396  elznn0nn  8035  elznn0  8036  zapne  8091  nneoor  8116  nn01to3  8328  ltxr  8465  xrletr  8494