Theorem orcom 871

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

Syntax hints:   ↔ wb 206   ∨ wo 848

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 849

This theorem is referenced by:  orcomd  872  orbi1i  914  orbi1d  917  orass  922  or32  926  or42  928  biorfri  940  pm5.7  956  oranabs  1002  ordir  1009  pm5.17  1014  dn1  1058  dfifp7  1070  3orrot  1092  3orel2OLD  1488  norcom  1532  norass  1539  cadan  1611  cadcomb  1615  nf2  1787  19.31v  1943  19.31  2242  2ralor  3212  eueq2  3670  uncom  4112  undif3  4254  reuun2  4279  dfif2  4483  reuprg  4662  rabrsn  4683  tppreqb  4763  ssunsn2  4785  disjor  5082  zfpair  5368  somin1  6098  ordtri2  6360  on0eqel  6450  fununi  6575  eliman0  6879  poxp2  8095  swoer  8677  supgtoreq  9386  cantnflem1d  9609  cantnflem1  9610  cflim2  10185  dffin7-2  10320  fpwwe2lem12  10565  suplem2pr  10976  leloe  11231  mulcan2g  11803  fimaxre  12098  fiminre  12101  arch  12410  elznn0nn  12514  elznn0  12515  nneo  12588  ltxr  13041  xrleloe  13070  xrrebnd  13095  xmullem2  13192  xmulcom  13193  xmulneg1  13196  xmulf  13199  sqeqori  14149  hashtpg  14420  odd2np1lem  16279  lcmcom  16532  dvdsprime  16626  coprm  16650  dvdszzq  16660  opprdomnb  20662  orngsqr  20811  lvecvscan2  21079  mplcoe1  22004  mplcoe5  22007  madutpos  22598  restntr  23138  alexsubALTlem2  24004  alexsubALTlem3  24005  xrsxmet  24766  dyaddisj  25565  mdegleb  26037  atandm3  26856  wilthlem2  27047  lgsdir2lem4  27307  noextenddif  27648  lesloe  27734  elzs2  28407  elznns  28410  tgcolg  28638  hlcomb  28687  axcontlem7  29055  elntg2  29070  nb3grprlem2  29466  vtxd0nedgb  29574  clwwlkneq0  30116  eupth2lem2  30306  eupth2lem3lem6  30320  numclwwlk3lem2lem  30470  hvmulcan2  31160  elat2  32427  chrelat2i  32452  atoml2i  32470  or3dir  32545  rmounid  32580  disjnf  32656  disjorf  32665  disjex  32678  disjexc  32679  disjunsn  32680  funcnv5mpt  32756  elicoelioo  32868  xrdifh  32870  tlt3  33062  ballotlemfc0  34670  ballotlemfcc  34671  bnj563  34919  subfacp1lem6  35398  dfon2lem5  35998  btwnconn1lem14  36313  outsideofcom  36341  outsideofeu  36344  lineunray  36360  ecase13d  36526  elicc3  36530  nn0prpw  36536  bj-dfbi5  36795  bj-consensusALT  36800  topdifinfeq  37599  onsucuni3  37616  wl-ifpimpr  37715  wl-cases2-dnf  37761  itg2addnclem2  37917  itgaddnclem2  37924  orfa  38327  notornotel2  38341  tsbi4  38381  ineleq  38599  disjecxrncnvep  38658  dfsucmap3  38708  dfdisjALTV5a  39048  dfeldisj5a  39059  leatb  39662  leat2  39664  isat3  39677  hlrelat2  39773  elpadd0  40179  aks6d1c2p2  42483  fsuppind  42942  safesnsupfilb  43768  ifporcor  43812  ifpim2  43822  ifpim23g  43845  ifpim123g  43850  rp-fakeoranass  43864  ontric3g  43872  stoweidlem26  46378  2reu3  47464  usgrexmpl2nb5  48390  itschlc0xyqsol1  49120  itschlc0xyqsol  49121  inlinecirc02plem  49140