Theorem orcom 883

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

Syntax hints:   ↔ wb 209   ∨ wo 860

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 210  df-or 861

This theorem is referenced by:  orcomd  884  orbi1i  926  orbi1d  929  orass  934  or32  938  or42  940  biorfri  952  pm5.7  968  oranabs  1015  ordir  1022  pm5.17  1027  dn1  1071  dfifp7  1083  3orrot  1106  3orel2OLD  1509  norcom  1553  norass  1560  cadan  1632  cadcomb  1636  nf2  1808  19.31v  1964  19.31  2272  2ralor  3239  eueq2  3676  uncom  4114  undif3  4255  reuun2  4280  dfif2  4485  reuprg  4665  rabrsn  4686  tppreqb  4768  ssunsn2  4788  disjor  5087  zfpair  5383  somin1  6124  ordtri2  6385  on0eqel  6475  fununi  6600  eliman0  6908  poxp2  8127  swoer  8714  supgtoreq  9419  cantnflem1d  9645  cantnflem1  9646  cflim2  10235  dffin7-2  10370  fpwwe2lem12  10615  suplem2pr  11026  leloe  11284  mulcan2g  11856  fimaxre  12150  fiminre  12153  arch  12492  elznn0nn  12596  elznn0  12597  nneo  12671  ltxr  13131  xrleloe  13160  xrrebnd  13185  xmullem2  13282  xmulcom  13283  xmulneg1  13286  xmulf  13289  sqeqori  14241  hashtpg  14512  odd2np1lem  16388  lcmcom  16641  dvdsprime  16735  coprm  16760  dvdszzq  16770  opprdomnb  20792  orngsqr  20938  lvecvscan2  21205  mplcoe1  22148  mplcoe5  22151  madutpos  22760  restntr  23300  alexsubALTlem2  24166  alexsubALTlem3  24167  xrsxmet  24928  dyaddisj  25716  mdegleb  26182  atandm3  27001  wilthlem2  27191  lgsdir2lem4  27450  noextenddif  27790  lesloe  27876  elzs2  28550  elznns  28553  tgcolg  28781  hlcomb  28830  plngcplem  29015  plngrotlem2  29018  axcontlem7  29229  elntg2  29244  nb3grprlem2  29640  vtxd0nedgb  29747  clwwlkneq0  30289  eupth2lem2  30479  eupth2lem3lem6  30493  numclwwlk3lem2lem  30643  hvmulcan2  31334  elat2  32601  chrelat2i  32626  atoml2i  32644  or3dir  32717  rmounid  32751  disjnf  32825  disjorf  32834  disjex  32847  disjexc  32848  disjunsn  32849  funcnv5mpt  32924  elicoelioo  33035  xrdifh  33037  tlt3  33203  ballotlemfc0  34800  ballotlemfcc  34801  bnj563  35049  subfacp1lem6  35548  dfon2lem5  36148  btwnconn1lem14  36463  outsideofcom  36491  outsideofeu  36494  lineunray  36510  ecase13d  36686  elicc3  36690  nn0prpw  36696  bj-dfbi5  37029  bj-consensusALT  37034  topdifinfeq  37856  onsucuni3  37873  wl-ifpimpr  37972  wl-cases2-dnf  38027  itg2addnclem2  38183  itgaddnclem2  38190  orfa  38593  notornotel2  38607  tsbi4  38647  ineleq  38865  disjecxrncnvep  38924  dfsucmap3  38974  dfdisjALTV5a  39314  dfeldisj5a  39325  leatb  39928  leat2  39930  isat3  39943  hlrelat2  40039  elpadd0  40445  aks6d1c2p2  42748  fsuppind  43184  safesnsupfilb  44006  ifporcor  44050  ifpim2  44060  ifpim23g  44083  ifpim123g  44088  rp-fakeoranass  44102  ontric3g  44110  stoweidlem26  46598  2reu3  47702  usgrexmpl2nb5  48656  itschlc0xyqsol1  49397  itschlc0xyqsol  49398  inlinecirc02plem  49417