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  2237  2ralor  3206  eueq2  3669  uncom  4108  undif3  4250  reuun2  4275  dfif2  4477  reuprg  4656  rabrsn  4677  tppreqb  4757  ssunsn2  4779  disjor  5073  zfpair  5359  somin1  6080  ordtri2  6341  on0eqel  6431  fununi  6556  eliman0  6859  poxp2  8073  swoer  8653  supgtoreq  9355  cantnflem1d  9578  cantnflem1  9579  cflim2  10151  dffin7-2  10286  fpwwe2lem12  10530  suplem2pr  10941  leloe  11196  mulcan2g  11768  fimaxre  12063  fiminre  12066  arch  12375  elznn0nn  12479  elznn0  12480  nneo  12554  ltxr  13011  xrleloe  13040  xrrebnd  13064  xmullem2  13161  xmulcom  13162  xmulneg1  13165  xmulf  13168  sqeqori  14118  hashtpg  14389  odd2np1lem  16248  lcmcom  16501  dvdsprime  16595  coprm  16619  dvdszzq  16629  opprdomnb  20630  orngsqr  20779  lvecvscan2  21047  mplcoe1  21970  mplcoe5  21973  madutpos  22555  restntr  23095  alexsubALTlem2  23961  alexsubALTlem3  23962  xrsxmet  24723  dyaddisj  25522  mdegleb  25994  atandm3  26813  wilthlem2  27004  lgsdir2lem4  27264  noextenddif  27605  sleloe  27691  elzs2  28321  elznns  28324  tgcolg  28530  hlcomb  28579  axcontlem7  28946  elntg2  28961  nb3grprlem2  29357  vtxd0nedgb  29465  clwwlkneq0  30004  eupth2lem2  30194  eupth2lem3lem6  30208  numclwwlk3lem2lem  30358  hvmulcan2  31048  elat2  32315  chrelat2i  32340  atoml2i  32358  or3dir  32434  rmounid  32469  disjnf  32545  disjorf  32554  disjex  32567  disjexc  32568  disjunsn  32569  funcnv5mpt  32645  elicoelioo  32756  xrdifh  32758  tlt3  32946  ballotlemfc0  34501  ballotlemfcc  34502  bnj563  34750  subfacp1lem6  35217  dfon2lem5  35820  btwnconn1lem14  36133  outsideofcom  36161  outsideofeu  36164  lineunray  36180  ecase13d  36346  elicc3  36350  nn0prpw  36356  bj-dfbi5  36607  bj-consensusALT  36612  topdifinfeq  37383  onsucuni3  37400  wl-ifpimpr  37499  wl-cases2-dnf  37545  itg2addnclem2  37711  itgaddnclem2  37718  orfa  38121  notornotel2  38135  tsbi4  38175  ineleq  38381  disjecxrncnvep  38421  leatb  39330  leat2  39332  isat3  39345  hlrelat2  39441  elpadd0  39847  aks6d1c2p2  42151  fsuppind  42622  safesnsupfilb  43450  ifporcor  43494  ifpim2  43504  ifpim23g  43527  ifpim123g  43532  rp-fakeoranass  43546  ontric3g  43554  stoweidlem26  46063  2reu3  47140  usgrexmpl2nb5  48066  itschlc0xyqsol1  48797  itschlc0xyqsol  48798  inlinecirc02plem  48817