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  3707  uncom  4154  undif3  4291  reuun2  4315  dfif2  4531  reuprg  4708  rabrsn  4729  tppreqb  4809  ssunsn2  4831  disjor  5129  zfpair  5420  somin1  6135  ordtri2  6400  on0eqel  6489  fununi  6624  eliman0  6932  poxp2  8129  swoer  8733  supgtoreq  9465  cantnflem1d  9683  cantnflem1  9684  cflim2  10258  dffin7-2  10393  fpwwe2lem12  10637  suplem2pr  11048  leloe  11300  mulcan2g  11868  fimaxre  12158  fiminre  12161  arch  12469  elznn0nn  12572  elznn0  12573  nneo  12646  ltxr  13095  xrleloe  13123  xrrebnd  13147  xmullem2  13244  xmulcom  13245  xmulneg1  13248  xmulf  13251  sqeqori  14178  hashtpg  14446  odd2np1lem  16283  lcmcom  16530  dvdsprime  16624  coprm  16648  lvecvscan2  20725  opprdomn  20919  mplcoe1  21592  mplcoe5  21595  madutpos  22144  restntr  22686  alexsubALTlem2  23552  alexsubALTlem3  23553  xrsxmet  24325  dyaddisj  25113  mdegleb  25582  atandm3  26383  wilthlem2  26573  lgsdir2lem4  26831  noextenddif  27171  sleloe  27257  tgcolg  27805  hlcomb  27854  axcontlem7  28228  elntg2  28243  nb3grprlem2  28638  vtxd0nedgb  28745  clwwlkneq0  29282  eupth2lem2  29472  eupth2lem3lem6  29486  numclwwlk3lem2lem  29636  hvmulcan2  30326  elat2  31593  chrelat2i  31618  atoml2i  31636  or3dir  31702  rmounid  31735  disjnf  31801  disjorf  31810  disjex  31823  disjexc  31824  disjunsn  31825  funcnv5mpt  31893  elicoelioo  31989  xrdifh  31991  dvdszzq  32021  tlt3  32140  orngsqr  32422  ballotlemfc0  33491  ballotlemfcc  33492  bnj563  33754  subfacp1lem6  34176  dfon2lem5  34759  btwnconn1lem14  35072  outsideofcom  35100  outsideofeu  35103  lineunray  35119  ecase13d  35198  elicc3  35202  nn0prpw  35208  bj-dfbi5  35451  bj-consensusALT  35456  topdifinfeq  36231  onsucuni3  36248  wl-ifpimpr  36347  wl-cases2-dnf  36381  itg2addnclem2  36540  itgaddnclem2  36547  orfa  36950  notornotel2  36964  tsbi4  37004  ineleq  37223  disjecxrncnvep  37260  leatb  38162  leat2  38164  isat3  38177  hlrelat2  38274  elpadd0  38680  aks6d1c2p2  40957  fsuppind  41162  safesnsupfilb  42169  ifporcor  42213  ifpim2  42223  ifpim23g  42246  ifpim123g  42251  rp-fakeoranass  42265  ontric3g  42273  elprn2  44350  stoweidlem26  44742  2reu3  45818  itschlc0xyqsol1  47452  itschlc0xyqsol  47453  inlinecirc02plem  47472