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  2066  dvelimfv  2067  dvelimor  2074  eueq2dc  2993  uncom  3367  reuun2  3508  prel12  3880  exmid01  4316  exmidsssnc  4321  ordtriexmid  4648  ordtri2orexmid  4650  ontr2exmid  4652  onsucsssucexmid  4654  ordsoexmid  4689  ordtri2or2exmid  4698  cnvsom  5311  fununi  5429  frec0g  6641  frecabcl  6643  frecsuclem  6650  swoer  6808  inffiexmid  7179  exmidontriimlem1  7541  enq0tr  7765  letr  8372  reapmul1  8886  reapneg  8888  reapcotr  8889  remulext1  8890  apsym  8897  mulext1  8903  elznn0nn  9608  elznn0  9609  zapne  9669  nneoor  9698  nn01to3  9967  ltxr  10127  xrletr  10160  swrdnd  11376  maxclpr  11932  minclpr  11947  odd2np1lem  12583  lcmcom  12786  dvdsprime  12844  coprm  12866  ballotfilemfc0  13176  ballotfilemfcc  13177  opprdomnbg  14506  bdbl  15480  cos11  15830  lgsdir2lem4  16016  vtxd0nedgbfi  16406  eupth2lem2dc  16566  eupth2lem3lem6fi  16578  subctctexmid  16886