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  1530  norass  1537  cadan  1609  cadcomb  1613  nf2  1785  19.31v  1941  19.31  2235  2ralor  3211  eueq2  3681  uncom  4121  undif3  4263  reuun2  4288  dfif2  4490  reuprg  4667  rabrsn  4688  tppreqb  4769  ssunsn2  4791  disjor  5089  zfpair  5376  somin1  6106  ordtri2  6367  on0eqel  6458  fununi  6591  eliman0  6898  poxp2  8122  swoer  8702  supgtoreq  9422  cantnflem1d  9641  cantnflem1  9642  cflim2  10216  dffin7-2  10351  fpwwe2lem12  10595  suplem2pr  11006  leloe  11260  mulcan2g  11832  fimaxre  12127  fiminre  12130  arch  12439  elznn0nn  12543  elznn0  12544  nneo  12618  ltxr  13075  xrleloe  13104  xrrebnd  13128  xmullem2  13225  xmulcom  13226  xmulneg1  13229  xmulf  13232  sqeqori  14179  hashtpg  14450  odd2np1lem  16310  lcmcom  16563  dvdsprime  16657  coprm  16681  dvdszzq  16691  opprdomnb  20626  lvecvscan2  21022  mplcoe1  21944  mplcoe5  21947  madutpos  22529  restntr  23069  alexsubALTlem2  23935  alexsubALTlem3  23936  xrsxmet  24698  dyaddisj  25497  mdegleb  25969  atandm3  26788  wilthlem2  26979  lgsdir2lem4  27239  noextenddif  27580  sleloe  27666  elzs2  28287  elznns  28290  tgcolg  28481  hlcomb  28530  axcontlem7  28897  elntg2  28912  nb3grprlem2  29308  vtxd0nedgb  29416  clwwlkneq0  29958  eupth2lem2  30148  eupth2lem3lem6  30162  numclwwlk3lem2lem  30312  hvmulcan2  31002  elat2  32269  chrelat2i  32294  atoml2i  32312  or3dir  32389  rmounid  32424  disjnf  32499  disjorf  32508  disjex  32521  disjexc  32522  disjunsn  32523  funcnv5mpt  32592  elicoelioo  32701  xrdifh  32703  tlt3  32896  orngsqr  33282  ballotlemfc0  34484  ballotlemfcc  34485  bnj563  34733  subfacp1lem6  35172  dfon2lem5  35775  btwnconn1lem14  36088  outsideofcom  36116  outsideofeu  36119  lineunray  36135  ecase13d  36301  elicc3  36305  nn0prpw  36311  bj-dfbi5  36562  bj-consensusALT  36567  topdifinfeq  37338  onsucuni3  37355  wl-ifpimpr  37454  wl-cases2-dnf  37500  itg2addnclem2  37666  itgaddnclem2  37673  orfa  38076  notornotel2  38090  tsbi4  38130  ineleq  38336  disjecxrncnvep  38376  leatb  39285  leat2  39287  isat3  39300  hlrelat2  39397  elpadd0  39803  aks6d1c2p2  42107  fsuppind  42578  safesnsupfilb  43407  ifporcor  43451  ifpim2  43461  ifpim23g  43484  ifpim123g  43489  rp-fakeoranass  43503  ontric3g  43511  elprn2  45632  stoweidlem26  46024  2reu3  47111  usgrexmpl2nb5  48027  itschlc0xyqsol1  48755  itschlc0xyqsol  48756  inlinecirc02plem  48775