Theorem orcom 718

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

Syntax hints:   ↔ wb 104   ∨ wo 698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  orcomd  719  orbi1i  753  orass  757  or32  760  or42  762  orbi1d  781  pm5.61  784  oranabs  805  ordir  807  pm2.1dc  827  notnotrdc  833  dcnnOLD  839  pm5.17dc  894  pm5.7dc  944  dn1dc  950  pm5.75  952  3orrot  974  3orcomb  977  excxor  1368  xorcom  1378  19.33b2  1617  nf4dc  1658  nf4r  1659  19.31r  1669  dveeq2  1803  sbequilem  1826  dvelimALT  1998  dvelimfv  1999  dvelimor  2006  eueq2dc  2899  uncom  3266  reuun2  3405  prel12  3751  exmid01  4177  exmidsssnc  4182  ordtriexmid  4498  ordtri2orexmid  4500  ontr2exmid  4502  onsucsssucexmid  4504  ordsoexmid  4539  ordtri2or2exmid  4548  cnvsom  5147  fununi  5256  frec0g  6365  frecabcl  6367  frecsuclem  6374  swoer  6529  inffiexmid  6872  exmidontriimlem1  7177  enq0tr  7375  letr  7981  reapmul1  8493  reapneg  8495  reapcotr  8496  remulext1  8497  apsym  8504  mulext1  8510  elznn0nn  9205  elznn0  9206  zapne  9265  nneoor  9293  nn01to3  9555  ltxr  9711  xrletr  9744  maxclpr  11164  minclpr  11178  odd2np1lem  11809  lcmcom  11996  dvdsprime  12054  coprm  12076  bdbl  13143  cos11  13414  lgsdir2lem4  13572  subctctexmid  13881