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  2022  dvelimfv  2023  dvelimor  2030  eueq2dc  2925  uncom  3294  reuun2  3433  prel12  3786  exmid01  4213  exmidsssnc  4218  ordtriexmid  4535  ordtri2orexmid  4537  ontr2exmid  4539  onsucsssucexmid  4541  ordsoexmid  4576  ordtri2or2exmid  4585  cnvsom  5187  fununi  5299  frec0g  6416  frecabcl  6418  frecsuclem  6425  swoer  6581  inffiexmid  6924  exmidontriimlem1  7238  enq0tr  7451  letr  8058  reapmul1  8570  reapneg  8572  reapcotr  8573  remulext1  8574  apsym  8581  mulext1  8587  elznn0nn  9285  elznn0  9286  zapne  9345  nneoor  9373  nn01to3  9635  ltxr  9793  xrletr  9826  maxclpr  11249  minclpr  11263  odd2np1lem  11895  lcmcom  12082  dvdsprime  12140  coprm  12162  bdbl  14400  cos11  14671  lgsdir2lem4  14829  subctctexmid  15148