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

Theorem orcom 400
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 399 . 2 ((𝜑𝜓) → (𝜓𝜑))
2 pm1.4 399 . 2 ((𝜓𝜑) → (𝜑𝜓))
31, 2impbii 197 1 ((𝜑𝜓) ↔ (𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 194  wo 381
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 195  df-or 383
This theorem is referenced by:  orcomd  401  orbi1i  540  orass  544  or32  547  or42  549  orbi1d  734  pm5.61  744  oranabs  896  ordir  904  pm5.17  927  pm5.7  970  pm5.75OLD  974  dn1  999  dfifp7  1012  3orrot  1036  3orcomb  1040  cadan  1538  cadcomb  1542  nf2  1701  19.31v  1856  19.31  2087  r19.30  3062  eueq2  3346  uncom  3718  undif3  3846  reuun2  3868  dfif2  4037  rabrsn  4202  tppreqb  4276  ssunsn2  4296  prel12  4318  disjor  4561  zfpair  4826  somin1  5435  ordtri2  5661  on0eqel  5748  fununi  5864  eliman0  6118  swoer  7636  supgtoreq  8236  cantnflem1d  8445  cantnflem1  8446  cflim2  8945  dffin7-2  9080  fpwwe2lem13  9320  suplem2pr  9731  leloe  9975  mulcan2g  10530  fimaxre  10817  arch  11136  elznn0nn  11224  elznn0  11225  nneo  11293  ltxr  11784  xrleloe  11812  xrrebnd  11832  xmullem2  11924  xmulcom  11925  xmulneg1  11928  xmulf  11931  sqeqori  12793  hashtpg  13071  odd2np1lem  14848  lcmcom  15090  dvdsprime  15184  coprm  15207  lvecvscan2  18879  opprdomn  19068  mplcoe1  19232  mplcoe5  19235  madutpos  20209  restntr  20738  alexsubALTlem2  21604  alexsubALTlem3  21605  xrsxmet  22352  dyaddisj  23087  mdegleb  23545  atandm3  24322  wilthlem2  24512  lgsdir2lem4  24770  tgcolg  25167  hlcomb  25216  axcontlem7  25568  nb3graprlem2  25747  eupath2lem2  26271  eupath2lem3  26272  hvmulcan2  27120  elat2  28389  chrelat2i  28414  atoml2i  28432  or3dir  28498  disjnf  28572  disjorf  28580  disjex  28593  disjexc  28594  disjunsn  28595  funcnv5mpt  28658  elicoelioo  28736  xrdifh  28738  tlt3  28802  orngsqr  28941  ballotlemfc0  29687  ballotlemfcc  29688  bnj563  29873  subfacp1lem6  30227  3orel2  30653  socnv  30714  dfon2lem5  30742  btwnconn1lem14  31183  outsideofcom  31211  outsideofeu  31214  lineunray  31230  ecase13d  31283  elicc3  31287  nn0prpw  31294  bj-dfbi5  31535  bj-consensusALT  31539  bj-nf2  31572  bj-nfn  31601  topdifinfeq  32177  onsucuni3  32194  wl-cases2-dnf  32277  itg2addnclem2  32435  itgaddnclem2  32442  orfa  32854  unitresl  32857  notornotel2  32871  tsbi4  32916  leatb  33400  leat2  33402  isat3  33415  hlrelat2  33510  elpadd0  33916  ifporcor  36628  ifpim2  36638  ifpim23g  36662  ifpim123g  36667  rp-fakeoranass  36681  elprn2  38505  stoweidlem26  38723  2reu3  39641  nb3grprlem2  40611  vtxd0nedgb  40705  eupth2lem2  41389  eupth2lem3lem6  41403
  Copyright terms: Public domain W3C validator