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  1983  dvelimfv  1984  dvelimor  1991  eueq2dc  2852  uncom  3215  reuun2  3354  prel12  3693  exmid01  4116  exmidsssnc  4121  ordtriexmid  4432  ordtri2orexmid  4433  ontr2exmid  4435  onsucsssucexmid  4437  ordsoexmid  4472  ordtri2or2exmid  4481  cnvsom  5077  fununi  5186  frec0g  6287  frecabcl  6289  frecsuclem  6296  swoer  6450  inffiexmid  6793  enq0tr  7235  letr  7840  reapmul1  8350  reapneg  8352  reapcotr  8353  remulext1  8354  apsym  8361  mulext1  8367  elznn0nn  9061  elznn0  9062  zapne  9118  nneoor  9146  nn01to3  9402  ltxr  9555  xrletr  9584  maxclpr  10987  minclpr  11001  odd2np1lem  11558  lcmcom  11734  dvdsprime  11792  coprm  11811  bdbl  12661  subctctexmid  13185