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  1485  norcom  1528  norass  1535  cadan  1607  cadcomb  1611  nf2  1783  nfnbiOLD  1854  19.31v  1940  19.31  2233  2ralor  3230  eueq2  3720  uncom  4169  undif3  4307  reuun2  4332  dfif2  4534  reuprg  4709  rabrsn  4730  tppreqb  4811  ssunsn2  4833  disjor  5131  zfpair  5428  somin1  6158  ordtri2  6424  on0eqel  6513  fununi  6646  eliman0  6951  poxp2  8173  swoer  8781  supgtoreq  9514  cantnflem1d  9732  cantnflem1  9733  cflim2  10307  dffin7-2  10442  fpwwe2lem12  10686  suplem2pr  11097  leloe  11351  mulcan2g  11921  fimaxre  12216  fiminre  12219  arch  12527  elznn0nn  12631  elznn0  12632  nneo  12706  ltxr  13161  xrleloe  13189  xrrebnd  13213  xmullem2  13310  xmulcom  13311  xmulneg1  13314  xmulf  13317  sqeqori  14256  hashtpg  14527  odd2np1lem  16380  lcmcom  16633  dvdsprime  16727  coprm  16751  dvdszzq  16761  opprdomnb  20740  lvecvscan2  21138  mplcoe1  22079  mplcoe5  22082  madutpos  22670  restntr  23212  alexsubALTlem2  24078  alexsubALTlem3  24079  xrsxmet  24853  dyaddisj  25653  mdegleb  26126  atandm3  26944  wilthlem2  27135  lgsdir2lem4  27395  noextenddif  27736  sleloe  27822  elzs2  28408  elznns  28411  tgcolg  28585  hlcomb  28634  axcontlem7  29008  elntg2  29023  nb3grprlem2  29421  vtxd0nedgb  29529  clwwlkneq0  30071  eupth2lem2  30261  eupth2lem3lem6  30275  numclwwlk3lem2lem  30425  hvmulcan2  31115  elat2  32382  chrelat2i  32407  atoml2i  32425  or3dir  32502  rmounid  32536  disjnf  32603  disjorf  32612  disjex  32625  disjexc  32626  disjunsn  32627  funcnv5mpt  32698  elicoelioo  32800  xrdifh  32802  tlt3  32958  orngsqr  33327  ballotlemfc0  34487  ballotlemfcc  34488  bnj563  34749  subfacp1lem6  35182  dfon2lem5  35781  btwnconn1lem14  36094  outsideofcom  36122  outsideofeu  36125  lineunray  36141  ecase13d  36308  elicc3  36312  nn0prpw  36318  bj-dfbi5  36569  bj-consensusALT  36574  topdifinfeq  37345  onsucuni3  37362  wl-ifpimpr  37461  wl-cases2-dnf  37505  itg2addnclem2  37671  itgaddnclem2  37678  orfa  38081  notornotel2  38095  tsbi4  38135  ineleq  38348  disjecxrncnvep  38384  leatb  39286  leat2  39288  isat3  39301  hlrelat2  39398  elpadd0  39804  aks6d1c2p2  42113  fsuppind  42591  safesnsupfilb  43422  ifporcor  43466  ifpim2  43476  ifpim23g  43499  ifpim123g  43504  rp-fakeoranass  43518  ontric3g  43526  elprn2  45601  stoweidlem26  45993  2reu3  47071  usgrexmpl2nb5  47944  itschlc0xyqsol1  48637  itschlc0xyqsol  48638  inlinecirc02plem  48657