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  2273  2ralor  3242  eueq2  3676  uncom  4115  undif3  4256  reuun2  4281  dfif2  4494  reuprg  4674  rabrsn  4695  tppreqb  4778  ssunsn2  4798  disjor  5096  zfpair  5397  somin1  6138  ordtri2  6403  on0eqel  6493  fununi  6618  eliman0  6925  poxp2  8148  swoer  8735  supgtoreq  9441  cantnflem1d  9667  cantnflem1  9668  cflim2  10265  dffin7-2  10400  fpwwe2lem12  10645  suplem2pr  11056  leloe  11314  mulcan2g  11886  fimaxre  12177  fiminre  12180  arch  12519  elznn0nn  12623  elznn0  12624  nneo  12698  ltxr  13158  xrleloe  13187  xrrebnd  13212  xmullem2  13309  xmulcom  13310  xmulneg1  13313  xmulf  13316  sqeqori  14270  hashtpg  14542  odd2np1lem  16423  lcmcom  16676  dvdsprime  16770  coprm  16795  dvdszzq  16805  opprdomnb  20852  orngsqr  21006  lvecvscan2  21273  mplcoe1  22225  mplcoe5  22228  madutpos  22836  restntr  23376  alexsubALTlem2  24242  alexsubALTlem3  24243  xrsxmet  25004  dyaddisj  25792  mdegleb  26258  atandm3  27080  wilthlem2  27270  lgsdir2lem4  27529  noextenddif  27869  lesloe  27955  elzs2  28629  elznns  28632  tgcolg  28860  hlcomb  28912  plngcplem  29104  plngrotlem2  29107  axcontlem7  29357  elntg2  29372  nb3grprlem2  29768  vtxd0nedgb  29875  clwwlkneq0  30417  eupth2lem2  30607  eupth2lem3lem6  30621  numclwwlk3lem2lem  30771  hvmulcan2  31462  elat2  32729  chrelat2i  32754  atoml2i  32772  or3dir  32845  rmounid  32878  disjnf  32952  disjorf  32961  disjex  32974  disjexc  32975  disjunsn  32976  funcnv5mpt  33049  elicoelioo  33160  xrdifh  33162  tlt3  33321  ballotlemfc0  34914  ballotlemfcc  34915  bnj563  35163  subfacp1lem6  35697  dfon2lem5  36297  btwnconn1lem14  36612  outsideofcom  36640  outsideofeu  36643  lineunray  36659  ltnadd  36730  elicc3  36868  nn0prpw  36874  bj-dfbi5  37207  bj-consensusALT  37212  topdifinfeq  38036  onsucuni3  38053  wl-ifpimpr  38152  wl-cases2-dnf  38207  itg2addnclem2  38363  itgaddnclem2  38370  orfa  38773  notornotel2  38785  tsbi4  38825  ineleq  39043  disjecxrncnvep  39102  dfsucmap3  39152  dfdisjALTV5a  39492  dfeldisj5a  39503  leatb  40106  leat2  40108  isat3  40121  hlrelat2  40217  elpadd0  40623  aks6d1c2p2  42926  fsuppind  43362  safesnsupfilb  44184  ifporcor  44228  ifpim2  44238  ifpim23g  44261  ifpim123g  44266  rp-fakeoranass  44280  ontric3g  44288  stoweidlem26  46780  2reu3  47887  usgrexmpl2nb5  48841  itschlc0xyqsol1  49586  itschlc0xyqsol  49587  inlinecirc02plem  49606