Theorem orcom 736

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

Syntax hints:   ↔ wb 105   ∨ wo 716

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 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orcomd  737  orbi1i  771  orass  775  or32  778  or42  780  orbi1d  799  pm5.61  802  oranabs  823  ordir  825  pm2.1dc  845  notnotrdc  851  dcnnOLD  857  pm5.17dc  912  pm5.7dc  963  dn1dc  969  pm5.75  971  3orrot  1011  3orcomb  1014  excxor  1423  xorcom  1433  19.33b2  1678  nf4dc  1718  nf4r  1719  19.31r  1729  dveeq2  1863  sbequilem  1886  dvelimALT  2063  dvelimfv  2064  dvelimor  2071  eueq2dc  2980  uncom  3353  reuun2  3492  prel12  3859  exmid01  4294  exmidsssnc  4299  ordtriexmid  4625  ordtri2orexmid  4627  ontr2exmid  4629  onsucsssucexmid  4631  ordsoexmid  4666  ordtri2or2exmid  4675  cnvsom  5287  fununi  5405  frec0g  6606  frecabcl  6608  frecsuclem  6615  swoer  6773  inffiexmid  7141  exmidontriimlem1  7479  enq0tr  7697  letr  8305  reapmul1  8818  reapneg  8820  reapcotr  8821  remulext1  8822  apsym  8829  mulext1  8835  elznn0nn  9536  elznn0  9537  zapne  9597  nneoor  9625  nn01to3  9894  ltxr  10053  xrletr  10086  swrdnd  11287  maxclpr  11843  minclpr  11858  odd2np1lem  12494  lcmcom  12697  dvdsprime  12755  coprm  12777  opprdomnbg  14350  bdbl  15294  cos11  15644  lgsdir2lem4  15830  vtxd0nedgbfi  16220  eupth2lem2dc  16380  eupth2lem3lem6fi  16392  subctctexmid  16702