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 ⊢ ((𝜑 ∨ 𝜓) ↔ (𝜓 ∨ 𝜑))

This proof depends on syntax axioms:   ↔ wb 105   ∨ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used 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  3896  exmid01  4335  exmidsssnc  4340  ordtriexmid  4668  ordtri2orexmid  4670  ontr2exmid  4672  onsucsssucexmid  4674  ordsoexmid  4709  ordtri2or2exmid  4718  cnvsom  5331  fununi  5449  frec0g  6668  frecabcl  6670  frecsuclem  6677  swoer  6835  inffiexmid  7213  exmidontriimlem1  7577  enq0tr  7801  letr  8408  reapmul1  8925  reapneg  8927  reapcotr  8928  remulext1  8929  apsym  8936  mulext1  8942  elznn0nn  9662  elznn0  9663  zapne  9723  nneoor  9752  nn01to3  10026  ltxr  10187  xrletr  10220  swrdnd  11445  maxclpr  12003  minclpr  12018  odd2np1lem  12655  lcmcom  12858  dvdsprime  12916  coprm  12939  ballotfilemfc0  13281  ballotfilemfcc  13282  opprdomnbg  14632  bdbl  15653  cos11  16004  lgsdir2lem4  16248  vtxd0nedgbfi  16638  eupth2lem2dc  16798  eupth2lem3lem6fi  16810  subctctexmid  17128