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  2977  uncom  3349  reuun2  3488  prel12  3852  exmid01  4286  exmidsssnc  4291  ordtriexmid  4617  ordtri2orexmid  4619  ontr2exmid  4621  onsucsssucexmid  4623  ordsoexmid  4658  ordtri2or2exmid  4667  cnvsom  5278  fununi  5395  frec0g  6558  frecabcl  6560  frecsuclem  6567  swoer  6725  inffiexmid  7093  exmidontriimlem1  7429  enq0tr  7647  letr  8255  reapmul1  8768  reapneg  8770  reapcotr  8771  remulext1  8772  apsym  8779  mulext1  8785  elznn0nn  9486  elznn0  9487  zapne  9547  nneoor  9575  nn01to3  9844  ltxr  10003  xrletr  10036  swrdnd  11233  maxclpr  11776  minclpr  11791  odd2np1lem  12426  lcmcom  12629  dvdsprime  12687  coprm  12709  opprdomnbg  14281  bdbl  15220  cos11  15570  lgsdir2lem4  15753  vtxd0nedgbfi  16110  subctctexmid  16551