Theorem orcom 730

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

Syntax hints:   ↔ wb 105   ∨ wo 710

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orcomd  731  orbi1i  765  orass  769  or32  772  or42  774  orbi1d  793  pm5.61  796  oranabs  817  ordir  819  pm2.1dc  839  notnotrdc  845  dcnnOLD  851  pm5.17dc  906  pm5.7dc  957  dn1dc  963  pm5.75  965  3orrot  987  3orcomb  990  excxor  1398  xorcom  1408  19.33b2  1653  nf4dc  1694  nf4r  1695  19.31r  1705  dveeq2  1839  sbequilem  1862  dvelimALT  2039  dvelimfv  2040  dvelimor  2047  eueq2dc  2948  uncom  3319  reuun2  3458  prel12  3815  exmid01  4247  exmidsssnc  4252  ordtriexmid  4574  ordtri2orexmid  4576  ontr2exmid  4578  onsucsssucexmid  4580  ordsoexmid  4615  ordtri2or2exmid  4624  cnvsom  5232  fununi  5348  frec0g  6493  frecabcl  6495  frecsuclem  6502  swoer  6658  inffiexmid  7015  exmidontriimlem1  7346  enq0tr  7560  letr  8168  reapmul1  8681  reapneg  8683  reapcotr  8684  remulext1  8685  apsym  8692  mulext1  8698  elznn0nn  9399  elznn0  9400  zapne  9460  nneoor  9488  nn01to3  9751  ltxr  9910  xrletr  9943  swrdnd  11126  maxclpr  11583  minclpr  11598  odd2np1lem  12233  lcmcom  12436  dvdsprime  12494  coprm  12516  opprdomnbg  14086  bdbl  15025  cos11  15375  lgsdir2lem4  15558  subctctexmid  16052