Theorem orcom 883

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

Syntax hints:   ↔ wb 209   ∨ wo 860

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 210  df-or 861

This theorem is referenced by:  orcomd  884  orbi1i  926  orbi1d  929  orass  934  or32  938  or42  940  biorfri  952  pm5.7  968  oranabs  1015  ordir  1024  pm5.17  1029  dn1  1073  dfifp7  1085  3orrot  1108  3orel2OLD  1516  norcom  1560  norass  1567  cadan  1639  cadcomb  1643  nf2  1815  19.31v  1971  19.31  2270  2ralor  3239  eueq2  3674  uncom  4113  undif3  4254  reuun2  4279  dfif2  4490  reuprg  4670  rabrsn  4691  tppreqb  4774  ssunsn2  4794  disjor  5092  zfpair  5394  somin1  6135  ordtri2  6398  on0eqel  6488  fununi  6613  eliman0  6920  poxp2  8140  swoer  8727  supgtoreq  9432  cantnflem1d  9658  cantnflem1  9659  cflim2  10248  dffin7-2  10383  fpwwe2lem12  10628  suplem2pr  11039  leloe  11297  mulcan2g  11869  fimaxre  12160  fiminre  12163  arch  12502  elznn0nn  12606  elznn0  12607  nneo  12681  ltxr  13141  xrleloe  13170  xrrebnd  13195  xmullem2  13292  xmulcom  13293  xmulneg1  13296  xmulf  13299  sqeqori  14252  hashtpg  14524  odd2np1lem  16399  lcmcom  16652  dvdsprime  16746  coprm  16771  dvdszzq  16781  opprdomnb  20802  orngsqr  20950  lvecvscan2  21217  mplcoe1  22169  mplcoe5  22172  madutpos  22780  restntr  23320  alexsubALTlem2  24186  alexsubALTlem3  24187  xrsxmet  24948  dyaddisj  25736  mdegleb  26202  atandm3  27021  wilthlem2  27211  lgsdir2lem4  27470  noextenddif  27810  lesloe  27896  elzs2  28570  elznns  28573  tgcolg  28801  hlcomb  28853  plngcplem  29045  plngrotlem2  29048  axcontlem7  29298  elntg2  29313  nb3grprlem2  29709  vtxd0nedgb  29816  clwwlkneq0  30358  eupth2lem2  30548  eupth2lem3lem6  30562  numclwwlk3lem2lem  30712  hvmulcan2  31403  elat2  32670  chrelat2i  32695  atoml2i  32713  or3dir  32786  rmounid  32819  disjnf  32893  disjorf  32902  disjex  32915  disjexc  32916  disjunsn  32917  funcnv5mpt  32990  elicoelioo  33101  xrdifh  33103  tlt3  33268  ballotlemfc0  34861  ballotlemfcc  34862  bnj563  35110  subfacp1lem6  35655  dfon2lem5  36255  btwnconn1lem14  36570  outsideofcom  36598  outsideofeu  36601  lineunray  36617  ltnadd  36673  elicc3  36806  nn0prpw  36812  bj-dfbi5  37145  bj-consensusALT  37150  topdifinfeq  37974  onsucuni3  37991  wl-ifpimpr  38090  wl-cases2-dnf  38145  itg2addnclem2  38301  itgaddnclem2  38308  orfa  38711  notornotel2  38723  tsbi4  38763  ineleq  38981  disjecxrncnvep  39040  dfsucmap3  39090  dfdisjALTV5a  39430  dfeldisj5a  39441  leatb  40044  leat2  40046  isat3  40059  hlrelat2  40155  elpadd0  40561  aks6d1c2p2  42864  fsuppind  43302  safesnsupfilb  44124  ifporcor  44168  ifpim2  44178  ifpim23g  44201  ifpim123g  44206  rp-fakeoranass  44220  ontric3g  44228  stoweidlem26  46720  2reu3  47824  usgrexmpl2nb5  48778  itschlc0xyqsol1  49523  itschlc0xyqsol  49524  inlinecirc02plem  49543