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  1643  nf4dc  1684  nf4r  1685  19.31r  1695  dveeq2  1829  sbequilem  1852  dvelimALT  2029  dvelimfv  2030  dvelimor  2037  eueq2dc  2937  uncom  3308  reuun2  3447  prel12  3802  exmid01  4232  exmidsssnc  4237  ordtriexmid  4558  ordtri2orexmid  4560  ontr2exmid  4562  onsucsssucexmid  4564  ordsoexmid  4599  ordtri2or2exmid  4608  cnvsom  5214  fununi  5327  frec0g  6464  frecabcl  6466  frecsuclem  6473  swoer  6629  inffiexmid  6976  exmidontriimlem1  7304  enq0tr  7518  letr  8126  reapmul1  8639  reapneg  8641  reapcotr  8642  remulext1  8643  apsym  8650  mulext1  8656  elznn0nn  9357  elznn0  9358  zapne  9417  nneoor  9445  nn01to3  9708  ltxr  9867  xrletr  9900  maxclpr  11404  minclpr  11419  odd2np1lem  12054  lcmcom  12257  dvdsprime  12315  coprm  12337  opprdomnbg  13906  bdbl  14823  cos11  15173  lgsdir2lem4  15356  subctctexmid  15731