Theorem orcom 733

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

Syntax hints:   ↔ wb 105   ∨ wo 713

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 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orcomd  734  orbi1i  768  orass  772  or32  775  or42  777  orbi1d  796  pm5.61  799  oranabs  820  ordir  822  pm2.1dc  842  notnotrdc  848  dcnnOLD  854  pm5.17dc  909  pm5.7dc  960  dn1dc  966  pm5.75  968  3orrot  1008  3orcomb  1011  excxor  1420  xorcom  1430  19.33b2  1675  nf4dc  1716  nf4r  1717  19.31r  1727  dveeq2  1861  sbequilem  1884  dvelimALT  2061  dvelimfv  2062  dvelimor  2069  eueq2dc  2976  uncom  3348  reuun2  3487  prel12  3849  exmid01  4283  exmidsssnc  4288  ordtriexmid  4614  ordtri2orexmid  4616  ontr2exmid  4618  onsucsssucexmid  4620  ordsoexmid  4655  ordtri2or2exmid  4664  cnvsom  5275  fununi  5392  frec0g  6554  frecabcl  6556  frecsuclem  6563  swoer  6721  inffiexmid  7084  exmidontriimlem1  7419  enq0tr  7637  letr  8245  reapmul1  8758  reapneg  8760  reapcotr  8761  remulext1  8762  apsym  8769  mulext1  8775  elznn0nn  9476  elznn0  9477  zapne  9537  nneoor  9565  nn01to3  9829  ltxr  9988  xrletr  10021  swrdnd  11212  maxclpr  11754  minclpr  11769  odd2np1lem  12404  lcmcom  12607  dvdsprime  12665  coprm  12687  opprdomnbg  14259  bdbl  15198  cos11  15548  lgsdir2lem4  15731  vtxd0nedgbfi  16085  subctctexmid  16479