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  norcom  1559  norass  1566  cadan  1641  cadcomb  1645  nf2  1817  19.31v  1973  19.31  2270  2ralor  3236  eueq2  3667  uncom  4157  undif3  4245  reuun2  4270  dfif2  4483  reuprg  4660  rabrsn  4681  tppreqb  4764  ssunsn2  4782  disjor  5084  zfpair  5382  somin1  6126  ordtri2  6398  on0eqel  6488  fununi  6615  eliman0  6922  poxp2  8162  swoer  8752  supgtoreq  9466  cantnflem1d  9692  cantnflem1  9693  cflim2  10344  dffin7-2  10479  fpwwe2lem12  10730  suplem2pr  11141  leloe  11399  mulcan2g  11973  fimaxre  12264  fiminre  12267  arch  12606  elznn0nn  12710  elznn0  12711  nneo  12786  ltxr  13247  xrleloe  13276  xrrebnd  13301  xmullem2  13398  xmulcom  13399  xmulneg1  13402  xmulf  13405  sqeqori  14361  hashtpg  14633  odd2np1lem  16515  lcmcom  16773  dvdsprime  16867  coprm  16892  dvdszzq  16902  opprdomnb  20973  orngsqr  21128  lvecvscan2  21395  mplcoe1  22351  mplcoe5  22354  madutpos  22962  restntr  23505  alexsubALTlem2  24372  alexsubALTlem3  24373  xrsxmet  25134  dyaddisj  25922  mdegleb  26387  atandm3  27211  wilthlem2  27401  lgsdir2lem4  27660  noextenddif  28030  lesloe  28116  elzs2  28790  elznns  28793  tgcolg  29022  hlcomb  29074  plngcplem  29268  plngrotlem2  29271  axcontlem7  29553  elntg2  29568  nb3grprlem2  29967  vtxd0nedgb  30074  clwwlkneq0  30625  eupth2lem2  30825  eupth2lem3lem6  30839  numclwwlk3lem2lem  30989  hvmulcan2  31680  elat2  32947  chrelat2i  32972  atoml2i  32990  or3dir  33105  rmounid  33138  disjnf  33211  disjorf  33220  disjex  33233  disjexc  33234  disjunsn  33235  funcnv5mpt  33308  elicoelioo  33416  xrdifh  33418  tlt3  33577  ballotlemfc0  35171  ballotlemfcc  35172  bnj563  35420  subfacp1lem6  36036  dfon2lem5  36641  btwnconn1lem14  36957  outsideofcom  36985  outsideofeu  36988  lineunray  37004  ltnadd  37059  elicc3  37197  nn0prpw  37203  bj-dfbi5  37536  bj-consensusALT  37541  topdifinfeq  38366  onsucuni3  38383  wl-ifpimpr  38482  wl-cases2-dnf  38537  itg2addnclem2  38683  itgaddnclem2  38690  orfa  39109  notornotel2  39121  tsbi4  39161  ineleq  39379  disjecxrncnvep  39438  dfsucmap3  39488  dfdisjALTV5a  39828  dfeldisj5a  39839  leatb  40442  leat2  40444  isat3  40457  hlrelat2  40553  elpadd0  40959  aks6d1c2p2  43262  fsuppind  43711  safesnsupfilb  44512  ifporcor  44556  ifpim2  44566  ifpim23g  44589  ifpim123g  44594  rp-fakeoranass  44608  ontric3g  44616  stoweidlem26  47129  goldratmolem4  48028  2reu3  48273  usgrexmpl2nb5  49227  itschlc0xyqsol1  49971  itschlc0xyqsol  49972