Theorem orcom 870

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

Syntax hints:   ↔ wb 206   ∨ wo 847

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 207  df-or 848

This theorem is referenced by:  orcomd  871  orbi1i  913  orbi1d  916  orass  921  or32  925  or42  927  biorfri  939  pm5.7  955  oranabs  1001  ordir  1008  pm5.17  1013  dn1  1057  dfifp7  1069  3orrot  1091  3orel2OLD  1487  norcom  1531  norass  1538  cadan  1610  cadcomb  1614  nf2  1786  19.31v  1942  19.31  2239  2ralor  3207  eueq2  3665  uncom  4107  undif3  4249  reuun2  4274  dfif2  4476  reuprg  4655  rabrsn  4676  tppreqb  4756  ssunsn2  4778  disjor  5075  zfpair  5361  somin1  6084  ordtri2  6346  on0eqel  6436  fununi  6561  eliman0  6865  poxp2  8079  swoer  8659  supgtoreq  9362  cantnflem1d  9585  cantnflem1  9586  cflim2  10161  dffin7-2  10296  fpwwe2lem12  10540  suplem2pr  10951  leloe  11206  mulcan2g  11778  fimaxre  12073  fiminre  12076  arch  12385  elznn0nn  12489  elznn0  12490  nneo  12563  ltxr  13016  xrleloe  13045  xrrebnd  13069  xmullem2  13166  xmulcom  13167  xmulneg1  13170  xmulf  13173  sqeqori  14123  hashtpg  14394  odd2np1lem  16253  lcmcom  16506  dvdsprime  16600  coprm  16624  dvdszzq  16634  opprdomnb  20634  orngsqr  20783  lvecvscan2  21051  mplcoe1  21973  mplcoe5  21976  madutpos  22558  restntr  23098  alexsubALTlem2  23964  alexsubALTlem3  23965  xrsxmet  24726  dyaddisj  25525  mdegleb  25997  atandm3  26816  wilthlem2  27007  lgsdir2lem4  27267  noextenddif  27608  sleloe  27694  elzs2  28324  elznns  28327  tgcolg  28533  hlcomb  28582  axcontlem7  28950  elntg2  28965  nb3grprlem2  29361  vtxd0nedgb  29469  clwwlkneq0  30011  eupth2lem2  30201  eupth2lem3lem6  30215  numclwwlk3lem2lem  30365  hvmulcan2  31055  elat2  32322  chrelat2i  32347  atoml2i  32365  or3dir  32441  rmounid  32476  disjnf  32552  disjorf  32561  disjex  32574  disjexc  32575  disjunsn  32576  funcnv5mpt  32652  elicoelioo  32765  xrdifh  32767  tlt3  32958  ballotlemfc0  34527  ballotlemfcc  34528  bnj563  34776  subfacp1lem6  35250  dfon2lem5  35850  btwnconn1lem14  36165  outsideofcom  36193  outsideofeu  36196  lineunray  36212  ecase13d  36378  elicc3  36382  nn0prpw  36388  bj-dfbi5  36639  bj-consensusALT  36644  topdifinfeq  37415  onsucuni3  37432  wl-ifpimpr  37531  wl-cases2-dnf  37577  itg2addnclem2  37732  itgaddnclem2  37739  orfa  38142  notornotel2  38156  tsbi4  38196  ineleq  38406  disjecxrncnvep  38457  dfsucmap3  38496  leatb  39411  leat2  39413  isat3  39426  hlrelat2  39522  elpadd0  39928  aks6d1c2p2  42232  fsuppind  42708  safesnsupfilb  43535  ifporcor  43579  ifpim2  43589  ifpim23g  43612  ifpim123g  43617  rp-fakeoranass  43631  ontric3g  43639  stoweidlem26  46148  2reu3  47234  usgrexmpl2nb5  48160  itschlc0xyqsol1  48891  itschlc0xyqsol  48892  inlinecirc02plem  48911