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  1864  sbequilem  1887  dvelimALT  2064  dvelimfv  2065  dvelimor  2072  eueq2dc  2989  uncom  3362  reuun2  3503  prel12  3874  exmid01  4310  exmidsssnc  4315  ordtriexmid  4642  ordtri2orexmid  4644  ontr2exmid  4646  onsucsssucexmid  4648  ordsoexmid  4683  ordtri2or2exmid  4692  cnvsom  5305  fununi  5423  frec0g  6627  frecabcl  6629  frecsuclem  6636  swoer  6794  inffiexmid  7165  exmidontriimlem1  7527  enq0tr  7748  letr  8355  reapmul1  8868  reapneg  8870  reapcotr  8871  remulext1  8872  apsym  8879  mulext1  8885  elznn0nn  9590  elznn0  9591  zapne  9651  nneoor  9679  nn01to3  9948  ltxr  10107  xrletr  10140  swrdnd  11347  maxclpr  11903  minclpr  11918  odd2np1lem  12554  lcmcom  12757  dvdsprime  12815  coprm  12837  opprdomnbg  14412  bdbl  15360  cos11  15710  lgsdir2lem4  15896  vtxd0nedgbfi  16286  eupth2lem2dc  16446  eupth2lem3lem6fi  16458  subctctexmid  16766