Theorem orcom 740

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

Syntax hints:   ↔ wb 105   ∨ wo 720

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 721

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orcomd  741  orbi1i  775  orass  779  or32  782  or42  784  orbi1d  803  pm5.61  806  oranabs  827  ordir  829  pm2.1dc  849  notnotrdc  855  dcnnOLD  861  pm5.17dc  916  pm5.7dc  967  dn1dc  973  pm5.75  975  3orrot  1015  3orcomb  1018  excxor  1427  xorcom  1437  19.33b2  1682  nf4dc  1722  nf4r  1723  19.31r  1733  dveeq2  1868  sbequilem  1891  dvelimALT  2070  dvelimfv  2071  dvelimor  2078  eueq2dc  2999  uncom  3373  reuun2  3516  prel12  3891  exmid01  4330  exmidsssnc  4335  ordtriexmid  4663  ordtri2orexmid  4665  ontr2exmid  4667  onsucsssucexmid  4669  ordsoexmid  4704  ordtri2or2exmid  4713  cnvsom  5326  fununi  5444  frec0g  6658  frecabcl  6660  frecsuclem  6667  swoer  6825  inffiexmid  7203  exmidontriimlem1  7567  enq0tr  7791  letr  8398  reapmul1  8913  reapneg  8915  reapcotr  8916  remulext1  8917  apsym  8924  mulext1  8930  elznn0nn  9637  elznn0  9638  zapne  9698  nneoor  9727  nn01to3  9996  ltxr  10156  xrletr  10189  swrdnd  11409  maxclpr  11966  minclpr  11981  odd2np1lem  12617  lcmcom  12820  dvdsprime  12878  coprm  12900  ballotfilemfc0  13210  ballotfilemfcc  13211  opprdomnbg  14556  bdbl  15527  cos11  15877  lgsdir2lem4  16064  vtxd0nedgbfi  16454  eupth2lem2dc  16614  eupth2lem3lem6fi  16626  subctctexmid  16944