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

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 ((𝜑𝜓) ↔ (𝜓𝜑))

Proof of Theorem orcom
StepHypRef Expression
1 pm1.4 401 . 2 ((𝜑𝜓) → (𝜓𝜑))
2 pm1.4 401 . 2 ((𝜓𝜑) → (𝜑𝜓))
31, 2impbii 199 1 ((𝜑𝜓) ↔ (𝜓𝜑))
Colors of variables: wff setvar class
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  738  pm5.61  748  oranabs  900  ordir  908  pm5.17  931  pm5.7  974  pm5.75OLD  978  dn1  1007  dfifp7  1018  3orrot  1042  3orcomb  1046  cadan  1546  cadcomb  1550  nf2  1709  nfnbi  1779  19.31v  1868  19.31  2100  r19.30  3077  eueq2  3374  uncom  3749  undif3  3880  reuun2  3902  dfif2  4079  rabrsn  4250  tppreqb  4327  ssunsn2  4350  prel12  4374  disjor  4625  zfpair  4895  somin1  5517  ordtri2  5746  on0eqel  5833  fununi  5952  eliman0  6210  swoer  7757  supgtoreq  8361  cantnflem1d  8570  cantnflem1  8571  cflim2  9070  dffin7-2  9205  fpwwe2lem13  9449  suplem2pr  9860  leloe  10109  mulcan2g  10666  fimaxre  10953  arch  11274  elznn0nn  11376  elznn0  11377  nneo  11446  ltxr  11934  xrleloe  11962  xrrebnd  11984  xmullem2  12080  xmulcom  12081  xmulneg1  12084  xmulf  12087  sqeqori  12959  hashtpg  13250  odd2np1lem  15045  lcmcom  15287  dvdsprime  15381  coprm  15404  lvecvscan2  19093  opprdomn  19282  mplcoe1  19446  mplcoe5  19449  madutpos  20429  restntr  20967  alexsubALTlem2  21833  alexsubALTlem3  21834  xrsxmet  22593  dyaddisj  23345  mdegleb  23805  atandm3  24586  wilthlem2  24776  lgsdir2lem4  25034  tgcolg  25430  hlcomb  25479  axcontlem7  25831  nb3grprlem2  26264  vtxd0nedgb  26365  eupth2lem2  27059  eupth2lem3lem6  27073  hvmulcan2  27900  elat2  29169  chrelat2i  29194  atoml2i  29212  or3dir  29278  disjnf  29356  disjorf  29364  disjex  29377  disjexc  29378  disjunsn  29379  funcnv5mpt  29443  elicoelioo  29514  xrdifh  29516  tlt3  29639  orngsqr  29778  ballotlemfc0  30528  ballotlemfcc  30529  bnj563  30787  subfacp1lem6  31141  3orel2  31567  dfon2lem5  31666  noextenddif  31795  sleloe  31853  btwnconn1lem14  32182  outsideofcom  32210  outsideofeu  32213  lineunray  32229  ecase13d  32282  elicc3  32286  nn0prpw  32293  bj-dfbi5  32534  bj-consensusALT  32538  topdifinfeq  33169  onsucuni3  33186  wl-cases2-dnf  33266  itg2addnclem2  33433  itgaddnclem2  33440  orfa  33852  unitresl  33855  notornotel2  33869  tsbi4  33914  leatb  34398  leat2  34400  isat3  34413  hlrelat2  34508  elpadd0  34914  ifporcor  37625  ifpim2  37635  ifpim23g  37659  ifpim123g  37664  rp-fakeoranass  37678  elprn2  39666  stoweidlem26  40006  2reu3  40951
  Copyright terms: Public domain W3C validator