Theorem orcom 884

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

This proof depends on syntax axioms:   ↔ wb 209   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  orcomd  885  orbi1i  927  orbi1d  930  orass  935  or32  939  or42  941  biorfri  953  pm5.7  968  oranabs  1015  ordir  1024  pm5.17  1029  dn1  1073  dfifp7  1085  3orrot  1108  norcom  1560  norass  1567  cadan  1642  cadcomb  1646  nf2  1818  19.31v  1976  19.31  2274  2ralor  3240  eueq2  3671  uncom  4160  undif3  4248  reuun2  4273  dfif2  4487  reuprg  4664  rabrsn  4685  tppreqb  4768  ssunsn2  4786  disjor  5088  zfpair  5387  somin1  6139  ordtri2  6416  on0eqel  6506  fununi  6637  eliman0  6945  poxp2  8187  swoer  8777  supgtoreq  9490  cantnflem1d  9716  cantnflem1  9717  cflim2  10368  dffin7-2  10503  fpwwe2lem12  10754  suplem2pr  11165  leloe  11423  mulcan2g  11997  fimaxre  12288  fiminre  12291  arch  12630  elznn0nn  12734  elznn0  12735  nneo  12810  ltxr  13271  xrleloe  13300  xrrebnd  13325  xmullem2  13422  xmulcom  13423  xmulneg1  13426  xmulf  13429  sqeqori  14385  hashtpg  14657  odd2np1lem  16539  lcmcom  16797  dvdsprime  16891  coprm  16916  dvdszzq  16926  opprdomnb  20998  orngsqr  21153  lvecvscan2  21420  mplcoe1  22376  mplcoe5  22379  madutpos  22987  restntr  23530  alexsubALTlem2  24397  alexsubALTlem3  24398  xrsxmet  25159  dyaddisj  25947  mdegleb  26412  atandm3  27236  wilthlem2  27426  lgsdir2lem4  27685  noextenddif  28055  lesloe  28141  elzs2  28815  elznns  28818  tgcolg  29047  hlcomb  29099  plngcplem  29293  plngrotlem2  29296  axcontlem7  29578  elntg2  29593  nb3grprlem2  29992  vtxd0nedgb  30099  clwwlkneq0  30650  eupth2lem2  30850  eupth2lem3lem6  30864  numclwwlk3lem2lem  31014  hvmulcan2  31705  elat2  32972  chrelat2i  32997  atoml2i  33015  or3dir  33130  rmounid  33163  disjnf  33236  disjorf  33245  disjex  33258  disjexc  33259  disjunsn  33260  funcnv5mpt  33333  elicoelioo  33440  xrdifh  33442  tlt3  33601  ballotlemfc0  35195  ballotlemfcc  35196  bnj563  35444  subfacp1lem6  36117  dfon2lem5  36727  btwnconn1lem14  37043  outsideofcom  37071  outsideofeu  37074  lineunray  37090  ltnadd  37145  elicc3  37283  nn0prpw  37289  bj-dfbi5  37622  bj-consensusALT  37627  topdifinfeq  38465  onsucuni3  38482  wl-ifpimpr  38581  wl-cases2-dnf  38636  itg2addnclem2  38782  itgaddnclem2  38789  orfa  39208  notornotel2  39220  tsbi4  39260  ineleq  39478  disjecxrncnvep  39537  dfsucmap3  39587  dfdisjALTV5a  39927  dfeldisj5a  39938  leatb  40541  leat2  40543  isat3  40556  hlrelat2  40652  elpadd0  41058  aks6d1c2p2  43361  fsuppind  43811  safesnsupfilb  44611  ifporcor  44655  ifpim2  44665  ifpim23g  44688  ifpim123g  44693  rp-fakeoranass  44707  ontric3g  44715  stoweidlem26  47241  goldratmolem4  48140  2reu3  48386  usgrexmpl2nb5  49339  itschlc0xyqsol1  50083  itschlc0xyqsol  50084