Theorem orcom 647

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

Syntax hints:   ↔ wb 98   ∨ wo 629

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 630

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  orcomd  648  orbi1i  680  orass  684  or32  687  or42  689  orbi1d  705  pm5.61  708  oranabs  728  ordir  730  pm2.1dc  745  notnotrdc  751  pm5.17dc  810  testbitestn  823  pm5.7dc  861  dn1dc  867  pm5.75  869  3orrot  891  3orcomb  894  excxor  1269  xorcom  1279  19.33b2  1520  nf4dc  1560  nf4r  1561  19.31r  1571  dveeq2  1696  sbequilem  1719  dvelimALT  1886  dvelimfv  1887  dvelimor  1894  eueq2dc  2714  uncom  3087  reuun2  3220  prel12  3542  ordtriexmid  4247  ordtri2orexmid  4248  ontr2exmid  4250  onsucsssucexmid  4252  ordsoexmid  4286  ordtri2or2exmid  4296  cnvsom  4861  fununi  4967  frec0g  5983  frecsuclem3  5990  swoer  6134  enq0tr  6532  letr  7101  reapmul1  7586  reapneg  7588  reapcotr  7589  remulext1  7590  apsym  7597  mulext1  7603  elznn0nn  8259  elznn0  8260  zapne  8315  nneoor  8340  nn01to3  8552  ltxr  8695  xrletr  8724