Theorem orcom 683

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

Syntax hints:   ↔ wb 104   ∨ wo 665

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  orcomd  684  orbi1i  716  orass  720  or32  723  or42  725  orbi1d  741  pm5.61  744  oranabs  765  ordir  767  pm2.1dc  784  notnotrdc  790  pm5.17dc  849  testbitestn  862  pm5.7dc  901  dn1dc  907  pm5.75  909  3orrot  931  3orcomb  934  excxor  1315  xorcom  1325  19.33b2  1566  nf4dc  1606  nf4r  1607  19.31r  1617  dveeq2  1744  sbequilem  1767  dvelimALT  1935  dvelimfv  1936  dvelimor  1943  eueq2dc  2789  uncom  3145  reuun2  3283  prel12  3621  exmid01  4038  ordtriexmid  4351  ordtri2orexmid  4352  ontr2exmid  4354  onsucsssucexmid  4356  ordsoexmid  4391  ordtri2or2exmid  4400  cnvsom  4987  fununi  5095  frec0g  6176  frecabcl  6178  frecsuclem  6185  swoer  6334  inffiexmid  6676  enq0tr  7054  letr  7629  reapmul1  8133  reapneg  8135  reapcotr  8136  remulext1  8137  apsym  8144  mulext1  8150  elznn0nn  8825  elznn0  8826  zapne  8882  nneoor  8909  nn01to3  9163  ltxr  9307  xrletr  9334  maxclpr  10716  odd2np1lem  11211  lcmcom  11385  dvdsprime  11443  coprm  11462