Theorem orcom 869

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

Syntax hints:   ↔ wb 205   ∨ wo 846

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 206  df-or 847

This theorem is referenced by:  orcomd  870  unitreslOLD  877  orbi1i  913  orbi1d  916  orass  921  or32  925  or42  927  pm5.7  953  oranabs  999  ordir  1006  pm5.17  1011  dn1  1057  dfifp7  1069  3orrot  1093  3orel2  1486  norcom  1531  norcomOLD  1532  norass  1539  cadan  1611  cadcomb  1615  nf2  1788  nfnbiOLD  1859  19.31v  1945  19.31  2228  2ralor  3229  eueq2  3705  uncom  4152  undif3  4289  reuun2  4313  dfif2  4529  reuprg  4706  rabrsn  4727  tppreqb  4807  ssunsn2  4829  disjor  5127  zfpair  5418  somin1  6131  ordtri2  6396  on0eqel  6485  fununi  6620  eliman0  6928  poxp2  8124  swoer  8729  supgtoreq  9461  cantnflem1d  9679  cantnflem1  9680  cflim2  10254  dffin7-2  10389  fpwwe2lem12  10633  suplem2pr  11044  leloe  11296  mulcan2g  11864  fimaxre  12154  fiminre  12157  arch  12465  elznn0nn  12568  elznn0  12569  nneo  12642  ltxr  13091  xrleloe  13119  xrrebnd  13143  xmullem2  13240  xmulcom  13241  xmulneg1  13244  xmulf  13247  sqeqori  14174  hashtpg  14442  odd2np1lem  16279  lcmcom  16526  dvdsprime  16620  coprm  16644  lvecvscan2  20713  opprdomn  20904  mplcoe1  21574  mplcoe5  21577  madutpos  22126  restntr  22668  alexsubALTlem2  23534  alexsubALTlem3  23535  xrsxmet  24307  dyaddisj  25095  mdegleb  25564  atandm3  26363  wilthlem2  26553  lgsdir2lem4  26811  noextenddif  27151  sleloe  27237  tgcolg  27785  hlcomb  27834  axcontlem7  28208  elntg2  28223  nb3grprlem2  28618  vtxd0nedgb  28725  clwwlkneq0  29262  eupth2lem2  29452  eupth2lem3lem6  29466  numclwwlk3lem2lem  29616  hvmulcan2  30304  elat2  31571  chrelat2i  31596  atoml2i  31614  or3dir  31680  rmounid  31713  disjnf  31779  disjorf  31788  disjex  31801  disjexc  31802  disjunsn  31803  funcnv5mpt  31871  elicoelioo  31967  xrdifh  31969  dvdszzq  31999  tlt3  32118  orngsqr  32391  ballotlemfc0  33429  ballotlemfcc  33430  bnj563  33692  subfacp1lem6  34114  dfon2lem5  34697  btwnconn1lem14  35010  outsideofcom  35038  outsideofeu  35041  lineunray  35057  ecase13d  35136  elicc3  35140  nn0prpw  35146  bj-dfbi5  35389  bj-consensusALT  35394  topdifinfeq  36169  onsucuni3  36186  wl-ifpimpr  36285  wl-cases2-dnf  36319  itg2addnclem2  36478  itgaddnclem2  36485  orfa  36888  notornotel2  36902  tsbi4  36942  ineleq  37161  disjecxrncnvep  37198  leatb  38100  leat2  38102  isat3  38115  hlrelat2  38212  elpadd0  38618  aks6d1c2p2  40895  fsuppind  41112  safesnsupfilb  42102  ifporcor  42146  ifpim2  42156  ifpim23g  42179  ifpim123g  42184  rp-fakeoranass  42198  ontric3g  42206  elprn2  44285  stoweidlem26  44677  2reu3  45753  itschlc0xyqsol1  47354  itschlc0xyqsol  47355  inlinecirc02plem  47374