MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  orcom Structured version   Visualization version   GIF version

Theorem orcom 888
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
StepHypRef Expression
1 pm1.4 887 . 2 ((𝜑𝜓) → (𝜓𝜑))
2 pm1.4 887 . 2 ((𝜓𝜑) → (𝜑𝜓))
31, 2impbii 200 1 ((𝜑𝜓) ↔ (𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 197  wo 865
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 198  df-or 866
This theorem is referenced by:  orcomd  889  orbi1i  928  orbi1d  931  orass  936  or32  940  or42  942  pm5.7  967  oranabs  1013  pm5.61  1014  ordir  1020  pm5.17  1026  dn1  1073  dfifp7  1085  3orrot  1105  3orcombOLD  1108  cadan  1703  cadcomb  1707  nf2  1865  nfnbi  1940  nfnbiOLD  1941  19.31v  2033  19.31  2270  r19.30  3270  eueq2  3578  uncom  3956  undif3  4090  reuun2  4111  dfif2  4281  rabrsn  4450  tppreqb  4526  ssunsn2  4548  prel12OLD  4570  disjor  4826  zfpair  5094  somin1  5740  ordtri2  5971  on0eqel  6054  fununi  6171  eliman0  6439  swoer  8005  supgtoreq  8611  cantnflem1d  8828  cantnflem1  8829  cflim2  9366  dffin7-2  9501  fpwwe2lem13  9745  suplem2pr  10156  leloe  10405  mulcan2g  10962  fimaxre  11249  arch  11552  elznn0nn  11653  elznn0  11654  nneo  11723  ltxr  12161  xrleloe  12189  xrrebnd  12213  xmullem2  12309  xmulcom  12310  xmulneg1  12313  xmulf  12316  sqeqori  13195  hashtpg  13480  odd2np1lem  15280  lcmcom  15521  dvdsprime  15614  coprm  15636  lvecvscan2  19315  opprdomn  19506  mplcoe1  19670  mplcoe5  19673  madutpos  20655  restntr  21196  alexsubALTlem2  22061  alexsubALTlem3  22062  xrsxmet  22821  dyaddisj  23573  mdegleb  24034  atandm3  24815  wilthlem2  25005  lgsdir2lem4  25263  tgcolg  25659  hlcomb  25708  axcontlem7  26060  nb3grprlem2  26495  vtxd0nedgb  26608  clwwlkneq0  27172  eupth2lem2  27388  eupth2lem3lem6  27402  numclwwlk3lem2lem  27567  hvmulcan2  28254  elat2  29523  chrelat2i  29548  atoml2i  29566  or3dir  29632  disjnf  29705  disjorf  29713  disjex  29726  disjexc  29727  disjunsn  29728  funcnv5mpt  29792  elicoelioo  29863  xrdifh  29865  tlt3  29986  orngsqr  30125  ballotlemfc0  30875  ballotlemfcc  30876  bnj563  31131  subfacp1lem6  31485  3orel2  31909  dfon2lem5  32007  noextenddif  32137  sleloe  32195  btwnconn1lem14  32523  outsideofcom  32551  outsideofeu  32554  lineunray  32570  ecase13d  32623  elicc3  32627  nn0prpw  32634  bj-dfbi5  32868  bj-consensusALT  32873  topdifinfeq  33509  onsucuni3  33526  wl-cases2-dnf  33606  itg2addnclem2  33769  itgaddnclem2  33776  orfa  34187  unitresl  34190  notornotel2  34204  tsbi4  34248  ineleq  34427  leatb  35067  leat2  35069  isat3  35082  hlrelat2  35178  elpadd0  35584  ifporcor  38300  ifpim2  38310  ifpim23g  38334  ifpim123g  38339  rp-fakeoranass  38353  elprn2  40340  stoweidlem26  40716  2reu3  41694
  Copyright terms: Public domain W3C validator