Theorem orcom 718

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

Syntax hints:   ↔ wb 104   ∨ wo 698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  orcomd  719  orbi1i  753  orass  757  or32  760  or42  762  orbi1d  781  pm5.61  784  oranabs  805  ordir  807  pm2.1dc  823  notnotrdc  829  dcnnOLD  835  pm5.17dc  890  pm5.7dc  939  dn1dc  945  pm5.75  947  3orrot  969  3orcomb  972  excxor  1360  xorcom  1370  19.33b2  1609  nf4dc  1650  nf4r  1651  19.31r  1661  dveeq2  1795  sbequilem  1818  dvelimALT  1990  dvelimfv  1991  dvelimor  1998  eueq2dc  2885  uncom  3252  reuun2  3391  prel12  3736  exmid01  4162  exmidsssnc  4167  ordtriexmid  4483  ordtri2orexmid  4485  ontr2exmid  4487  onsucsssucexmid  4489  ordsoexmid  4524  ordtri2or2exmid  4533  cnvsom  5132  fununi  5241  frec0g  6347  frecabcl  6349  frecsuclem  6356  swoer  6511  inffiexmid  6854  exmidontriimlem1  7159  enq0tr  7357  letr  7963  reapmul1  8475  reapneg  8477  reapcotr  8478  remulext1  8479  apsym  8486  mulext1  8492  elznn0nn  9187  elznn0  9188  zapne  9244  nneoor  9272  nn01to3  9533  ltxr  9689  xrletr  9719  maxclpr  11134  minclpr  11148  odd2np1lem  11776  lcmcom  11957  dvdsprime  12015  coprm  12035  bdbl  12999  cos11  13270  subctctexmid  13670