MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bicomi Unicode version

Theorem bicomi 196
Description: Inference from commutative law for logical equivalence. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
bicomi.1
Assertion
Ref Expression
bicomi

Proof of Theorem bicomi
StepHypRef Expression
1 bicomi.1 . 2
2 bicom1 193 . 2
31, 2ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 178
This theorem is referenced by:  biimpri  200  bitr2i  244  bitr3i  245  bitr4i  246  syl5bbr  253  syl5rbbr  254  syl6bbr  257  syl6rbbr  258  mtbir  293  sylnibr  299  sylnbir  301  xchnxbir  303  xchbinxr  305  con1bii  324  con2bii  325  nbn  340  xor3  350  pm5.41  357  pm4.64  365  pm4.63  414  pm4.61  419  anor  479  pm4.53  482  pm4.55  484  pm4.56  485  pm4.57  487  pm4.25  505  pm4.87  571  anidm  629  pm4.77  770  anabs1  791  anabs7  793  pm4.76  846  pm5.63  900  jaoi2OLD  945  3ianor  967  3oran  969  pm3.2an3  1152  syl3anbr  1247  3an6  1284  nannot  1324  truimfal  1381  nottru  1384  nic-dfim  1470  nic-dfneg  1471  2nalexn  1614  2nexaln  1616  sbequ8  1698  dvelimf  2017  cleljust  2048  cleljustALT  2049  sb5rf  2112  sb6rf  2114  sb10f  2158  nne  2591  necon3bbii  2618  necon2abii  2645  necon2bbii  2646  nabbi  2685  nnel  2693  alexeq  3067  ceqsrexbv  3072  clel2  3074  clel4  3077  2reu5lem1  3142  2reu5lem2  3143  2reu5lem3  3144  dfsbcq2  3167  cbvreucsf  3298  nss  3391  raldifb  3473  difab  3596  un0  3639  in0  3640  ss0b  3644  ssunsn2  4007  iindif2  4214  nssss  4520  opthneg  4543  epse  4674  restidsing  5134  cotr  5182  issref  5183  mptpreima  5303  ralrnmpt  5822  fmptsng  5869  weniso  6013  uniuni  6355  suppvalbr  6663  eroveu  7156  isfinite2  7529  marypha1lem  7630  marypha2lem4  7635  wemapso2lem  7714  en3lplem2  7768  cantnfp1  7836  carden2  8104  fseqenlem1  8141  iscard3  8210  cardnum  8211  alephinit  8212  cardinfima  8214  alephiso  8215  dfac10b  8255  dfackm  8282  isfin5-2  8507  brdom7disj  8645  brdom6disj  8646  hashtpg  12127  wrdeqswrdlsw  12284  wrd2ind  12313  splfv1  12338  cshwsexa  12399  s4f1o  12469  vdwapun  13975  cshwsiun  14066  cshwshash  14071  grpss  15496  pmtrfrn  15901  pmtrrn2  15903  pmtrprfvalrn  15931  drngnidl  17120  drnglpir  17144  unocv  17813  dsmmacl  17874  toptopon  18242  ordtbas2  18499  ordtrest2  18512  restutopopn  19513  xmeterval  19707  ovolfcl  20650  eldv  21073  eltayl  21566  musumsum  22273  usgrafilem1  23003  trls  23114  is2wlk  23143  lejdii  24620  mdslle1i  25400  mdslle2i  25401  mdslj1i  25402  mdslj2i  25403  spc2ed  25536  mo5f  25548  unipreima  25641  2ndpreima  25682  issrg  25897  ordtrest2NEW  26062  ordtconlem1  26063  ballotlem2  26574  plymulx0  26651  relexpindlem  27043  fprod2dlem  27193  cnvco1  27272  cnvco2  27273  dfiota3  27656  nabi1i  27940  nabi2i  27941  trer  28182  inixp  28293  notbinot1  28550  impor  28552  notbinot2  28554  truconj  28575  sbcalf  28591  sbcexf  28592  exlimddvfi  28601  sbccom2lem  28604  sbccom2  28605  sbccom2f  28606  tsim1  28612  tsxo3  28621  tsxo4  28622  sbcom3OLD  28651  an43  28665  rmxypairf1o  28925  acsfn1p  29229  pm10.252  29286  pm10.253  29287  pm10.42  29289  aaanv  29314  pm13.195  29340  pm13.196a  29341  aibandbiaiffaiffb  29582  aovov0bi  29776  rexdifpr  29798  dff14a  29818  f13dfv  29821  rabasiun  29904  wwlknndef  30043  wlknwwlknvbij  30046  el2wlkonotot0  30065  usg2spthonot0  30082  clwwlknndef  30110  clwwlkvbij  30137  frgraun  30262  frgra2v  30265  4cycl2vnunb  30283  vdn0frgrav2  30290  vdgn0frgrav2  30291  2spotdisj  30328  usg2spot2nb  30332  usgreg2spot  30334  frgraregord013  30385  pgrpgt2nabel  30431  0rngnnzr  30438  lindslinindsimp2lem5  30580  islininds2  30602  ldepslinc  30635  sbc3or  30814  sbc3orgOLD  30815  en3lpVD  31159  3orbi123VD  31164  sbc3orgVD  31165  undif3VD  31196  ax6e2ndeqVD  31223  ax6e2ndeqALT  31245  sineq0ALT  31251  bnj115  31292  bnj156  31297  bnj206  31300  bnj110  31429  bnj121  31441  bnj124  31442  bnj130  31445  bnj153  31451  bnj207  31452  bnj581  31479  bnj611  31489  bnj864  31493  bnj865  31494  bnj893  31499  bnj1000  31512  bnj978  31520  bnj1040  31541  bnj1049  31543  bnj1133  31558  bnj1189  31578  bj-nf3  31671  bj-nfdt  31708  bj-cleljust  31781  bj-denotes  31845  bj-issetw  31846  bj-ralcom4  31852  bj-rexcom4  31853  bj-elsngl  31908  isopos  32262  islvol5  32660  elpadd0  32890  dvhopellsm  34199  diblsmopel  34253  mapdvalc  34711
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 179
  Copyright terms: Public domain W3C validator