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  3219  eueq2  3698  uncom  4138  undif3  4280  reuun2  4305  dfif2  4507  reuprg  4684  rabrsn  4705  tppreqb  4786  ssunsn2  4808  disjor  5106  zfpair  5396  somin1  6127  ordtri2  6392  on0eqel  6483  fununi  6616  eliman0  6921  poxp2  8147  swoer  8755  supgtoreq  9488  cantnflem1d  9707  cantnflem1  9708  cflim2  10282  dffin7-2  10417  fpwwe2lem12  10661  suplem2pr  11072  leloe  11326  mulcan2g  11896  fimaxre  12191  fiminre  12194  arch  12503  elznn0nn  12607  elznn0  12608  nneo  12682  ltxr  13136  xrleloe  13165  xrrebnd  13189  xmullem2  13286  xmulcom  13287  xmulneg1  13290  xmulf  13293  sqeqori  14237  hashtpg  14508  odd2np1lem  16364  lcmcom  16617  dvdsprime  16711  coprm  16735  dvdszzq  16745  opprdomnb  20682  lvecvscan2  21078  mplcoe1  22000  mplcoe5  22003  madutpos  22585  restntr  23125  alexsubALTlem2  23991  alexsubALTlem3  23992  xrsxmet  24754  dyaddisj  25554  mdegleb  26026  atandm3  26845  wilthlem2  27036  lgsdir2lem4  27296  noextenddif  27637  sleloe  27723  elzs2  28344  elznns  28347  tgcolg  28538  hlcomb  28587  axcontlem7  28954  elntg2  28969  nb3grprlem2  29365  vtxd0nedgb  29473  clwwlkneq0  30015  eupth2lem2  30205  eupth2lem3lem6  30219  numclwwlk3lem2lem  30369  hvmulcan2  31059  elat2  32326  chrelat2i  32351  atoml2i  32369  or3dir  32446  rmounid  32481  disjnf  32556  disjorf  32565  disjex  32578  disjexc  32579  disjunsn  32580  funcnv5mpt  32651  elicoelioo  32760  xrdifh  32762  tlt3  32955  orngsqr  33331  ballotlemfc0  34530  ballotlemfcc  34531  bnj563  34779  subfacp1lem6  35212  dfon2lem5  35810  btwnconn1lem14  36123  outsideofcom  36151  outsideofeu  36154  lineunray  36170  ecase13d  36336  elicc3  36340  nn0prpw  36346  bj-dfbi5  36597  bj-consensusALT  36602  topdifinfeq  37373  onsucuni3  37390  wl-ifpimpr  37489  wl-cases2-dnf  37535  itg2addnclem2  37701  itgaddnclem2  37708  orfa  38111  notornotel2  38125  tsbi4  38165  ineleq  38377  disjecxrncnvep  38413  leatb  39315  leat2  39317  isat3  39330  hlrelat2  39427  elpadd0  39833  aks6d1c2p2  42137  fsuppind  42588  safesnsupfilb  43417  ifporcor  43461  ifpim2  43471  ifpim23g  43494  ifpim123g  43499  rp-fakeoranass  43513  ontric3g  43521  elprn2  45643  stoweidlem26  46035  2reu3  47119  usgrexmpl2nb5  48020  itschlc0xyqsol1  48726  itschlc0xyqsol  48727  inlinecirc02plem  48746