Theorem orcom 903

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

Syntax hints:   ↔ wb 198   ∨ wo 880

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 199  df-or 881

This theorem is referenced by:  orcomd  904  orbi1i  944  orbi1d  947  orass  952  or32  956  or42  958  pm5.7  983  oranabs  1029  pm5.61  1030  ordir  1036  pm5.17  1042  dn1  1086  dfifp7  1098  3orrot  1118  3orcombOLD  1121  cadan  1724  cadcomb  1728  nf2  1886  nfnbi  1956  nfnbiOLD  1957  19.31v  2042  19.31  2279  r19.30  3292  eueq2  3605  uncom  3984  undif3  4118  reuun2  4139  dfif2  4308  rabrsn  4477  tppreqb  4554  ssunsn2  4576  prel12OLD  4598  disjor  4855  zfpair  5125  somin1  5771  ordtri2  5998  on0eqel  6080  fununi  6197  eliman0  6469  swoer  8039  supgtoreq  8645  cantnflem1d  8862  cantnflem1  8863  cflim2  9400  dffin7-2  9535  fpwwe2lem13  9779  suplem2pr  10190  leloe  10443  mulcan2g  11006  fimaxre  11298  arch  11615  elznn0nn  11718  elznn0  11719  nneo  11789  ltxr  12235  xrleloe  12263  xrrebnd  12287  xmullem2  12383  xmulcom  12384  xmulneg1  12387  xmulf  12390  sqeqori  13270  hashtpg  13556  odd2np1lem  15438  lcmcom  15679  dvdsprime  15772  coprm  15794  lvecvscan2  19471  opprdomn  19662  mplcoe1  19826  mplcoe5  19829  madutpos  20816  restntr  21357  alexsubALTlem2  22222  alexsubALTlem3  22223  xrsxmet  22982  dyaddisj  23762  mdegleb  24223  atandm3  25018  wilthlem2  25208  lgsdir2lem4  25466  tgcolg  25866  hlcomb  25915  axcontlem7  26269  elntg2  26284  nb3grprlem2  26679  vtxd0nedgb  26786  clwwlkneq0  27371  eupth2lem2  27596  eupth2lem3lem6  27610  numclwwlk3lem2lem  27798  hvmulcan2  28485  elat2  29754  chrelat2i  29779  atoml2i  29797  or3dir  29863  disjnf  29931  disjorf  29939  disjex  29952  disjexc  29953  disjunsn  29954  funcnv5mpt  30017  elicoelioo  30087  xrdifh  30089  tlt3  30210  orngsqr  30349  ballotlemfc0  31100  ballotlemfcc  31101  bnj563  31359  subfacp1lem6  31713  3orel2  32136  dfon2lem5  32230  noextenddif  32360  sleloe  32418  btwnconn1lem14  32746  outsideofcom  32774  outsideofeu  32777  lineunray  32793  ecase13d  32846  elicc3  32850  nn0prpw  32856  bj-dfbi5  33087  bj-consensusALT  33092  topdifinfeq  33743  onsucuni3  33760  wl-cases2-dnf  33840  itg2addnclem2  34005  itgaddnclem2  34012  orfa  34423  unitresl  34426  notornotel2  34439  tsbi4  34483  ineleq  34667  leatb  35367  leat2  35369  isat3  35382  hlrelat2  35478  elpadd0  35884  ifporcor  38648  ifpim2  38658  ifpim23g  38682  ifpim123g  38687  rp-fakeoranass  38701  elprn2  40661  stoweidlem26  41037  2reu3  42013