Theorem orcom 723

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

Syntax hints:   ↔ wb 104   ∨ wo 703

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 704

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  orcomd  724  orbi1i  758  orass  762  or32  765  or42  767  orbi1d  786  pm5.61  789  oranabs  810  ordir  812  pm2.1dc  832  notnotrdc  838  dcnnOLD  844  pm5.17dc  899  pm5.7dc  949  dn1dc  955  pm5.75  957  3orrot  979  3orcomb  982  excxor  1373  xorcom  1383  19.33b2  1622  nf4dc  1663  nf4r  1664  19.31r  1674  dveeq2  1808  sbequilem  1831  dvelimALT  2003  dvelimfv  2004  dvelimor  2011  eueq2dc  2903  uncom  3271  reuun2  3410  prel12  3758  exmid01  4184  exmidsssnc  4189  ordtriexmid  4505  ordtri2orexmid  4507  ontr2exmid  4509  onsucsssucexmid  4511  ordsoexmid  4546  ordtri2or2exmid  4555  cnvsom  5154  fununi  5266  frec0g  6376  frecabcl  6378  frecsuclem  6385  swoer  6541  inffiexmid  6884  exmidontriimlem1  7198  enq0tr  7396  letr  8002  reapmul1  8514  reapneg  8516  reapcotr  8517  remulext1  8518  apsym  8525  mulext1  8531  elznn0nn  9226  elznn0  9227  zapne  9286  nneoor  9314  nn01to3  9576  ltxr  9732  xrletr  9765  maxclpr  11186  minclpr  11200  odd2np1lem  11831  lcmcom  12018  dvdsprime  12076  coprm  12098  bdbl  13297  cos11  13568  lgsdir2lem4  13726  subctctexmid  14034