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 199 1 ((𝜑𝜓) ↔ (𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 196  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 197  df-or 384
This theorem is referenced by:  orcomd  402  orbi1i  541  orass  545  or32  548  or42  550  orbi1d  739  pm5.61  749  oranabs  919  ordir  927  pm5.17  950  pm5.7  995  dn1  1028  dfifp7  1039  3orrot  1061  3orcombOLD  1066  cadan  1588  cadcomb  1592  nf2  1751  nfnbi  1821  19.31v  1910  19.31  2140  r19.30  3111  eueq2  3413  uncom  3790  undif3  3921  reuun2  3943  dfif2  4121  rabrsn  4291  tppreqb  4368  ssunsn2  4391  prel12  4414  disjor  4666  zfpair  4934  somin1  5564  ordtri2  5796  on0eqel  5883  fununi  6002  eliman0  6261  swoer  7817  supgtoreq  8417  cantnflem1d  8623  cantnflem1  8624  cflim2  9123  dffin7-2  9258  fpwwe2lem13  9502  suplem2pr  9913  leloe  10162  mulcan2g  10719  fimaxre  11006  arch  11327  elznn0nn  11429  elznn0  11430  nneo  11499  ltxr  11987  xrleloe  12015  xrrebnd  12037  xmullem2  12133  xmulcom  12134  xmulneg1  12137  xmulf  12140  sqeqori  13016  hashtpg  13305  odd2np1lem  15111  lcmcom  15353  dvdsprime  15447  coprm  15470  lvecvscan2  19160  opprdomn  19349  mplcoe1  19513  mplcoe5  19516  madutpos  20496  restntr  21034  alexsubALTlem2  21899  alexsubALTlem3  21900  xrsxmet  22659  dyaddisj  23410  mdegleb  23869  atandm3  24650  wilthlem2  24840  lgsdir2lem4  25098  tgcolg  25494  hlcomb  25543  axcontlem7  25895  nb3grprlem2  26327  vtxd0nedgb  26440  clwwlkneq0  26990  eupth2lem2  27197  eupth2lem3lem6  27211  numclwwlk3lemlem  27370  hvmulcan2  28058  elat2  29327  chrelat2i  29352  atoml2i  29370  or3dir  29436  disjnf  29510  disjorf  29518  disjex  29531  disjexc  29532  disjunsn  29533  funcnv5mpt  29597  elicoelioo  29668  xrdifh  29670  tlt3  29793  orngsqr  29932  ballotlemfc0  30682  ballotlemfcc  30683  bnj563  30939  subfacp1lem6  31293  3orel2  31718  dfon2lem5  31816  noextenddif  31946  sleloe  32004  btwnconn1lem14  32332  outsideofcom  32360  outsideofeu  32363  lineunray  32379  ecase13d  32432  elicc3  32436  nn0prpw  32443  bj-dfbi5  32684  bj-consensusALT  32688  topdifinfeq  33328  onsucuni3  33345  wl-cases2-dnf  33425  itg2addnclem2  33592  itgaddnclem2  33599  orfa  34011  unitresl  34014  notornotel2  34028  tsbi4  34073  ineleq  34259  leatb  34897  leat2  34899  isat3  34912  hlrelat2  35007  elpadd0  35413  ifporcor  38123  ifpim2  38133  ifpim23g  38157  ifpim123g  38162  rp-fakeoranass  38176  elprn2  40184  stoweidlem26  40561  2reu3  41509
  Copyright terms: Public domain W3C validator