Theorem orcom 634

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

Syntax hints:   ↔ wb 98   ∨ wo 616

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 617

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  orcomd  635  orbi1i  667  orass  671  or32  674  or42  676  orbi1d  692  pm5.61  695  oranabs  716  ordir  718  testbitestn  732  pm2.1dc  736  notnot2dc  742  pm5.17dc  803  pm5.7dc  849  dn1dc  855  pm5.75  857  3orrot  879  3orcomb  882  excxor  1254  xorcom  1262  19.33b2  1502  nf4dc  1542  nf4r  1543  19.31r  1553  dveeq2  1678  sbequilem  1701  dvelimALT  1868  dvelimfv  1869  dvelimor  1876  eueq2dc  2691  uncom  3064  reuun2  3197  prel12  3516  ordtriexmid  4194  ordtri2orexmid  4195  onsucsssucexmid  4196  ordsoexmid  4224  cnvsom  4788  fununi  4893  frec0g  5902  frecsuclem3  5906  swoer  6045  enq0tr  6289  letr  6699  dcnbidcnn  7006