Theorem orcom 729

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

Syntax hints:   ↔ wb 105   ∨ wo 709

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 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orcomd  730  orbi1i  764  orass  768  or32  771  or42  773  orbi1d  792  pm5.61  795  oranabs  816  ordir  818  pm2.1dc  838  notnotrdc  844  dcnnOLD  850  pm5.17dc  905  pm5.7dc  956  dn1dc  962  pm5.75  964  3orrot  986  3orcomb  989  excxor  1389  xorcom  1399  19.33b2  1640  nf4dc  1681  nf4r  1682  19.31r  1692  dveeq2  1826  sbequilem  1849  dvelimALT  2026  dvelimfv  2027  dvelimor  2034  eueq2dc  2934  uncom  3304  reuun2  3443  prel12  3798  exmid01  4228  exmidsssnc  4233  ordtriexmid  4554  ordtri2orexmid  4556  ontr2exmid  4558  onsucsssucexmid  4560  ordsoexmid  4595  ordtri2or2exmid  4604  cnvsom  5210  fununi  5323  frec0g  6452  frecabcl  6454  frecsuclem  6461  swoer  6617  inffiexmid  6964  exmidontriimlem1  7283  enq0tr  7496  letr  8104  reapmul1  8616  reapneg  8618  reapcotr  8619  remulext1  8620  apsym  8627  mulext1  8633  elznn0nn  9334  elznn0  9335  zapne  9394  nneoor  9422  nn01to3  9685  ltxr  9844  xrletr  9877  maxclpr  11369  minclpr  11383  odd2np1lem  12016  lcmcom  12205  dvdsprime  12263  coprm  12285  opprdomnbg  13773  bdbl  14682  cos11  15029  lgsdir2lem4  15188  subctctexmid  15561