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

Theorem orcom 401
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 400 . 2 ((𝜑𝜓) → (𝜓𝜑))
2 pm1.4 400 . 2 ((𝜓𝜑) → (𝜑𝜓))
31, 2impbii 198 1 ((𝜑𝜓) ↔ (𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 195  wo 382
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 196  df-or 384
This theorem is referenced by:  orcomd  402  orbi1i  541  orass  545  or32  548  or42  550  orbi1d  735  pm5.61  745  oranabs  897  ordir  905  pm5.17  928  pm5.7  971  pm5.75OLD  975  dn1  1000  dfifp7  1013  3orrot  1037  3orcomb  1041  cadan  1539  cadcomb  1543  nf2  1702  19.31v  1857  19.31  2089  r19.30  3063  eueq2  3347  uncom  3719  undif3  3847  reuun2  3869  dfif2  4038  rabrsn  4203  tppreqb  4277  ssunsn2  4299  prel12  4323  disjor  4567  zfpair  4831  somin1  5448  ordtri2  5675  on0eqel  5762  fununi  5878  eliman0  6133  swoer  7659  supgtoreq  8259  cantnflem1d  8468  cantnflem1  8469  cflim2  8968  dffin7-2  9103  fpwwe2lem13  9343  suplem2pr  9754  leloe  10003  mulcan2g  10560  fimaxre  10847  arch  11166  elznn0nn  11268  elznn0  11269  nneo  11337  ltxr  11825  xrleloe  11853  xrrebnd  11873  xmullem2  11967  xmulcom  11968  xmulneg1  11971  xmulf  11974  sqeqori  12838  hashtpg  13121  odd2np1lem  14902  lcmcom  15144  dvdsprime  15238  coprm  15261  lvecvscan2  18933  opprdomn  19122  mplcoe1  19286  mplcoe5  19289  madutpos  20267  restntr  20796  alexsubALTlem2  21662  alexsubALTlem3  21663  xrsxmet  22420  dyaddisj  23170  mdegleb  23628  atandm3  24405  wilthlem2  24595  lgsdir2lem4  24853  tgcolg  25249  hlcomb  25298  axcontlem7  25650  nb3graprlem2  25981  eupath2lem2  26505  eupath2lem3  26506  hvmulcan2  27314  elat2  28583  chrelat2i  28608  atoml2i  28626  or3dir  28692  disjnf  28766  disjorf  28774  disjex  28787  disjexc  28788  disjunsn  28789  funcnv5mpt  28852  elicoelioo  28930  xrdifh  28932  tlt3  28996  orngsqr  29135  ballotlemfc0  29881  ballotlemfcc  29882  bnj563  30067  subfacp1lem6  30421  3orel2  30847  socnv  30908  dfon2lem5  30936  btwnconn1lem14  31377  outsideofcom  31405  outsideofeu  31408  lineunray  31424  ecase13d  31477  elicc3  31481  nn0prpw  31488  bj-dfbi5  31729  bj-consensusALT  31733  bj-nf2  31766  bj-nfn  31795  topdifinfeq  32374  onsucuni3  32391  wl-cases2-dnf  32474  itg2addnclem2  32632  itgaddnclem2  32639  orfa  33051  unitresl  33054  notornotel2  33068  tsbi4  33113  leatb  33597  leat2  33599  isat3  33612  hlrelat2  33707  elpadd0  34113  ifporcor  36825  ifpim2  36835  ifpim23g  36859  ifpim123g  36864  rp-fakeoranass  36878  elprn2  38701  stoweidlem26  38919  2reu3  39837  nb3grprlem2  40609  vtxd0nedgb  40703  eupth2lem2  41387  eupth2lem3lem6  41401
  Copyright terms: Public domain W3C validator