Theorem orcom 717

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

Syntax hints:   ↔ wb 104   ∨ wo 697

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  orcomd  718  orbi1i  752  orass  756  or32  759  or42  761  orbi1d  780  pm5.61  783  oranabs  804  ordir  806  pm2.1dc  822  notnotrdc  828  dcnnOLD  834  pm5.17dc  889  pm5.7dc  938  dn1dc  944  pm5.75  946  3orrot  968  3orcomb  971  excxor  1356  xorcom  1366  19.33b2  1608  nf4dc  1648  nf4r  1649  19.31r  1659  dveeq2  1787  sbequilem  1810  dvelimALT  1985  dvelimfv  1986  dvelimor  1993  eueq2dc  2857  uncom  3220  reuun2  3359  prel12  3698  exmid01  4121  exmidsssnc  4126  ordtriexmid  4437  ordtri2orexmid  4438  ontr2exmid  4440  onsucsssucexmid  4442  ordsoexmid  4477  ordtri2or2exmid  4486  cnvsom  5082  fununi  5191  frec0g  6294  frecabcl  6296  frecsuclem  6303  swoer  6457  inffiexmid  6800  enq0tr  7242  letr  7847  reapmul1  8357  reapneg  8359  reapcotr  8360  remulext1  8361  apsym  8368  mulext1  8374  elznn0nn  9068  elznn0  9069  zapne  9125  nneoor  9153  nn01to3  9409  ltxr  9562  xrletr  9591  maxclpr  10994  minclpr  11008  odd2np1lem  11569  lcmcom  11745  dvdsprime  11803  coprm  11822  bdbl  12672  subctctexmid  13196