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  3orel2OLD  1516  norcom  1560  norass  1567  cadan  1642  cadcomb  1646  nf2  1818  19.31v  1974  19.31  2272  2ralor  3238  eueq2  3671  uncom  4108  undif3  4249  reuun2  4274  dfif2  4487  reuprg  4667  rabrsn  4688  tppreqb  4771  ssunsn2  4791  disjor  5089  zfpair  5390  somin1  6131  ordtri2  6397  on0eqel  6487  fununi  6612  eliman0  6919  poxp2  8145  swoer  8732  supgtoreq  9445  cantnflem1d  9671  cantnflem1  9672  cflim2  10269  dffin7-2  10404  fpwwe2lem12  10655  suplem2pr  11066  leloe  11324  mulcan2g  11896  fimaxre  12187  fiminre  12190  arch  12529  elznn0nn  12633  elznn0  12634  nneo  12709  ltxr  13170  xrleloe  13199  xrrebnd  13224  xmullem2  13321  xmulcom  13322  xmulneg1  13325  xmulf  13328  sqeqori  14282  hashtpg  14554  odd2np1lem  16436  lcmcom  16689  dvdsprime  16783  coprm  16808  dvdszzq  16818  opprdomnb  20884  orngsqr  21038  lvecvscan2  21305  mplcoe1  22259  mplcoe5  22262  madutpos  22870  restntr  23413  alexsubALTlem2  24280  alexsubALTlem3  24281  xrsxmet  25042  dyaddisj  25830  mdegleb  26296  atandm3  27123  wilthlem2  27313  lgsdir2lem4  27572  noextenddif  27912  lesloe  27998  elzs2  28672  elznns  28675  tgcolg  28904  hlcomb  28956  plngcplem  29150  plngrotlem2  29153  axcontlem7  29435  elntg2  29450  nb3grprlem2  29849  vtxd0nedgb  29956  clwwlkneq0  30507  eupth2lem2  30707  eupth2lem3lem6  30721  numclwwlk3lem2lem  30871  hvmulcan2  31562  elat2  32829  chrelat2i  32854  atoml2i  32872  or3dir  32945  rmounid  32978  disjnf  33051  disjorf  33060  disjex  33073  disjexc  33074  disjunsn  33075  funcnv5mpt  33148  elicoelioo  33257  xrdifh  33259  tlt3  33418  ballotlemfc0  35012  ballotlemfcc  35013  bnj563  35261  subfacp1lem6  35772  dfon2lem5  36372  btwnconn1lem14  36688  outsideofcom  36716  outsideofeu  36719  lineunray  36735  ltnadd  36806  elicc3  36944  nn0prpw  36950  bj-dfbi5  37283  bj-consensusALT  37288  topdifinfeq  38112  onsucuni3  38129  wl-ifpimpr  38228  wl-cases2-dnf  38283  itg2addnclem2  38429  itgaddnclem2  38436  orfa  38840  notornotel2  38852  tsbi4  38892  ineleq  39110  disjecxrncnvep  39169  dfsucmap3  39219  dfdisjALTV5a  39559  dfeldisj5a  39570  leatb  40173  leat2  40175  isat3  40188  hlrelat2  40284  elpadd0  40690  aks6d1c2p2  42993  fsuppind  43444  safesnsupfilb  44266  ifporcor  44310  ifpim2  44320  ifpim23g  44343  ifpim123g  44348  rp-fakeoranass  44362  ontric3g  44370  stoweidlem26  46862  goldratmolem4  47761  2reu3  48006  usgrexmpl2nb5  48960  itschlc0xyqsol1  49704  itschlc0xyqsol  49705  inlinecirc02plem  49724