Theorem orcom 402

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	|- ( ( ph \/ ps ) <-> ( ps \/ ph ) )

Proof of Theorem orcom

Step	Hyp	Ref	Expression
1		pm1.4 401	. 2 |- ( ( ph \/ ps ) -> ( ps \/ ph ) )
2		pm1.4 401	. 2 |- ( ( ps \/ ph ) -> ( ph \/ ps ) )
3	1, 2	impbii 199	1 |- ( ( ph \/ ps ) <-> ( ps \/ ph ) )

Syntax hints:   <-> wb 196   \/ wo 383

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 197  df-or 385

This theorem is referenced by:  orcomd  403  orbi1i  542  orass  546  or32  549  or42  551  orbi1d  739  pm5.61  749  oranabs  901  ordir  909  pm5.17  932  pm5.7  975  pm5.75OLD  979  dn1  1008  dfifp7  1019  3orrot  1044  3orcomb  1048  cadan  1548  cadcomb  1552  nf2  1711  nfnbi  1781  19.31v  1870  19.31  2102  r19.30  3082  eueq2  3380  uncom  3757  undif3  3888  reuun2  3910  dfif2  4088  rabrsn  4259  tppreqb  4336  ssunsn2  4359  prel12  4383  disjor  4634  zfpair  4904  somin1  5529  ordtri2  5758  on0eqel  5845  fununi  5964  eliman0  6223  swoer  7772  supgtoreq  8376  cantnflem1d  8585  cantnflem1  8586  cflim2  9085  dffin7-2  9220  fpwwe2lem13  9464  suplem2pr  9875  leloe  10124  mulcan2g  10681  fimaxre  10968  arch  11289  elznn0nn  11391  elznn0  11392  nneo  11461  ltxr  11949  xrleloe  11977  xrrebnd  11999  xmullem2  12095  xmulcom  12096  xmulneg1  12099  xmulf  12102  sqeqori  12976  hashtpg  13267  odd2np1lem  15064  lcmcom  15306  dvdsprime  15400  coprm  15423  lvecvscan2  19112  opprdomn  19301  mplcoe1  19465  mplcoe5  19468  madutpos  20448  restntr  20986  alexsubALTlem2  21852  alexsubALTlem3  21853  xrsxmet  22612  dyaddisj  23364  mdegleb  23824  atandm3  24605  wilthlem2  24795  lgsdir2lem4  25053  tgcolg  25449  hlcomb  25498  axcontlem7  25850  nb3grprlem2  26283  vtxd0nedgb  26384  eupth2lem2  27079  eupth2lem3lem6  27093  hvmulcan2  27930  elat2  29199  chrelat2i  29224  atoml2i  29242  or3dir  29308  disjnf  29384  disjorf  29392  disjex  29405  disjexc  29406  disjunsn  29407  funcnv5mpt  29469  elicoelioo  29540  xrdifh  29542  tlt3  29665  orngsqr  29804  ballotlemfc0  30554  ballotlemfcc  30555  bnj563  30813  subfacp1lem6  31167  3orel2  31592  dfon2lem5  31692  noextenddif  31821  sleloe  31879  btwnconn1lem14  32207  outsideofcom  32235  outsideofeu  32238  lineunray  32254  ecase13d  32307  elicc3  32311  nn0prpw  32318  bj-dfbi5  32559  bj-consensusALT  32563  topdifinfeq  33198  onsucuni3  33215  wl-cases2-dnf  33295  itg2addnclem2  33462  itgaddnclem2  33469  orfa  33881  unitresl  33884  notornotel2  33898  tsbi4  33943  ineleq  34119  leatb  34579  leat2  34581  isat3  34594  hlrelat2  34689  elpadd0  35095  ifporcor  37806  ifpim2  37816  ifpim23g  37840  ifpim123g  37845  rp-fakeoranass  37859  elprn2  39866  stoweidlem26  40243  2reu3  41188