Theorem orcom 876

Description: Commutative law for disjunction. Theorem *4.31 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 15-Nov-2012.)

Assertion

Ref	Expression
orcom	⊢ ((𝜑 ∨ 𝜓) ↔ (𝜓 ∨ 𝜑))

Proof of Theorem orcom

Step	Hyp	Ref	Expression
1		pm1.4 875	. 2 ⊢ ((𝜑 ∨ 𝜓) → (𝜓 ∨ 𝜑))
2		pm1.4 875	. 2 ⊢ ((𝜓 ∨ 𝜑) → (𝜑 ∨ 𝜓))
3	1, 2	impbii 210	1 ⊢ ((𝜑 ∨ 𝜓) ↔ (𝜓 ∨ 𝜑))

Syntax hints:   ↔ wb 207   ∨ wo 853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 208  df-or 854

This theorem is referenced by:  orcomd  877  orbi1i  919  orbi1d  922  orass  927  or32  931  or42  933  biorfri  945  pm5.7  961  oranabs  1007  ordir  1014  pm5.17  1019  dn1  1063  dfifp7  1075  3orrot  1097  3orel2OLD  1493  norcom  1537  norass  1544  cadan  1616  cadcomb  1620  nf2  1792  19.31v  1948  19.31  2246  2ralor  3214  eueq2  3658  uncom  4095  undif3  4235  reuun2  4260  dfif2  4463  reuprg  4642  rabrsn  4663  tppreqb  4745  ssunsn2  4765  disjor  5061  zfpair  5357  somin1  6090  ordtri2  6352  on0eqel  6442  fununi  6567  eliman0  6871  poxp2  8090  swoer  8672  supgtoreq  9381  cantnflem1d  9607  cantnflem1  9608  cflim2  10183  dffin7-2  10318  fpwwe2lem12  10563  suplem2pr  10974  leloe  11230  mulcan2g  11802  fimaxre  12098  fiminre  12101  arch  12432  elznn0nn  12536  elznn0  12537  nneo  12611  ltxr  13064  xrleloe  13093  xrrebnd  13118  xmullem2  13215  xmulcom  13216  xmulneg1  13219  xmulf  13222  sqeqori  14174  hashtpg  14445  odd2np1lem  16307  lcmcom  16560  dvdsprime  16654  coprm  16679  dvdszzq  16689  opprdomnb  20696  orngsqr  20845  lvecvscan2  21112  mplcoe1  22020  mplcoe5  22023  madutpos  22632  restntr  23172  alexsubALTlem2  24038  alexsubALTlem3  24039  xrsxmet  24800  dyaddisj  25588  mdegleb  26054  atandm3  26867  wilthlem2  27057  lgsdir2lem4  27316  noextenddif  27657  lesloe  27743  elzs2  28416  elznns  28419  tgcolg  28647  hlcomb  28696  axcontlem7  29064  elntg2  29079  nb3grprlem2  29475  vtxd0nedgb  29582  clwwlkneq0  30124  eupth2lem2  30314  eupth2lem3lem6  30328  numclwwlk3lem2lem  30478  hvmulcan2  31169  elat2  32436  chrelat2i  32461  atoml2i  32479  or3dir  32554  rmounid  32589  disjnf  32666  disjorf  32675  disjex  32688  disjexc  32689  disjunsn  32690  funcnv5mpt  32766  elicoelioo  32877  xrdifh  32879  tlt3  33056  ballotlemfc0  34684  ballotlemfcc  34685  bnj563  34933  subfacp1lem6  35420  dfon2lem5  36020  btwnconn1lem14  36335  outsideofcom  36363  outsideofeu  36366  lineunray  36382  ecase13d  36548  elicc3  36552  nn0prpw  36558  bj-dfbi5  36892  bj-consensusALT  36897  topdifinfeq  37719  onsucuni3  37736  wl-ifpimpr  37835  wl-cases2-dnf  37890  itg2addnclem2  38046  itgaddnclem2  38053  orfa  38456  notornotel2  38470  tsbi4  38510  ineleq  38728  disjecxrncnvep  38787  dfsucmap3  38837  dfdisjALTV5a  39177  dfeldisj5a  39188  leatb  39791  leat2  39793  isat3  39806  hlrelat2  39902  elpadd0  40308  aks6d1c2p2  42611  fsuppind  43047  safesnsupfilb  43869  ifporcor  43913  ifpim2  43923  ifpim23g  43946  ifpim123g  43951  rp-fakeoranass  43965  ontric3g  43973  stoweidlem26  46476  2reu3  47580  usgrexmpl2nb5  48534  itschlc0xyqsol1  49264  itschlc0xyqsol  49265  inlinecirc02plem  49284