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

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

Proof of Theorem bicomi
StepHypRef Expression
1 bicomi.1 . 2
2 bicom1 199 . 2
31, 2ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184
This theorem is referenced by:  biimpri  206  bitr2i  250  bitr3i  251  bitr4i  252  syl5bbr  259  syl5rbbr  260  syl6bbr  263  syl6rbbr  264  mtbir  299  sylnibr  305  sylnbir  307  xchnxbir  309  xchbinxr  311  con1bii  331  con2bii  332  nbn  347  xor3  357  pm5.41  364  pm4.64  372  pm4.63  421  pm4.61  426  anor  489  pm4.53  492  pm4.55  494  pm4.56  495  pm4.57  497  pm4.25  515  pm4.87  584  anidm  644  pm4.77  787  anabs1  808  anabs7  810  pm4.76  866  pm5.63  924  3ianor  990  3oran  992  pm3.2an3  1175  syl3anbr  1272  3an6  1309  nannot  1351  nanbi  1352  truan  1412  truimfal  1428  nottru  1431  nic-dfim  1502  nic-dfneg  1503  2nalexn  1649  2nexaln  1651  sbequ8  1744  dvelimf  2076  cleljust  2109  cleljustALT  2110  sb5rf  2165  sb6rf  2166  sb10f  2200  abeq1i  2586  nne  2658  necon3bbii  2718  necon2abii  2723  necon2bbii  2724  nabbiOLD  2791  nnel  2802  nnelOLD  2803  alexeq  3229  ceqsrexbv  3234  clel2  3236  clel4  3239  2reu5lem1  3305  2reu5lem2  3306  2reu5lem3  3307  dfsbcq2  3330  cbvreucsf  3468  nss  3561  raldifb  3643  difab  3766  un0  3810  in0  3811  ss0b  3815  ssunsn2  4189  rabasiun  4334  iindif2  4399  nssss  4708  opthneg  4731  epse  4867  restidsing  5335  cotrg  5383  issref  5385  mptpreima  5505  ralrnmpt  6040  fmptsng  6092  fmptsnd  6093  dff14a  6177  f13dfv  6180  weniso  6250  uniuni  6609  suppvalbr  6922  eroveu  7425  isfinite2  7798  marypha1lem  7913  marypha2lem4  7918  wemapso2lem  7999  en3lplem2  8053  cantnfp1  8121  carden2  8389  fseqenlem1  8426  iscard3  8495  cardnum  8496  alephinit  8497  cardinfima  8499  alephiso  8500  dfac10b  8540  dfackm  8567  isfin5-2  8792  brdom7disj  8930  brdom6disj  8931  fsuppmapnn0fiubex  12098  hashtpg  12523  wrdeqswrdlsw  12674  wrd2ind  12703  splfv1  12731  cshwsexa  12792  s4f1o  12866  vdwapun  14492  cshwsiun  14584  cshwshash  14589  grpss  16071  pmtrfrn  16483  pmtrrn2  16485  pmtrprfvalrn  16513  issrg  17159  drngnidl  17877  drnglpir  17901  0ringnnzr  17917  unocv  18711  dsmmacl  18772  pmatcollpw2lem  19278  fvmptnn04if  19350  toptopon  19434  ordtbas2  19692  ordtrest2  19705  xmeterval  20935  ovolfcl  21878  eldv  22302  eltayl  22755  musumsum  23468  usgrafilem1  24411  trls  24538  is2wlk  24567  wwlknndef  24737  wlknwwlknvbij  24740  clwwlknndef  24773  clwwlkvbij  24801  el2wlkonotot0  24872  usg2spthonot0  24889  frgraun  24996  frgra2v  24999  4cycl2vnunb  25017  vdn0frgrav2  25023  vdgn0frgrav2  25024  2spotdisj  25061  usg2spot2nb  25065  usgreg2spot  25067  frgraregord013  25118  lejdii  26456  mdslle1i  27236  mdslle2i  27237  mdslj1i  27238  mdslj2i  27239  mo5f  27383  unipreima  27484  2ndpreima  27525  xrge0infss  27580  ordtrest2NEW  27905  ordtconlem1  27906  ballotlem2  28427  plymulx0  28504  relexpindlem  29062  cnvco1  29189  cnvco2  29190  dfiota3  29573  nabi1i  29857  nabi2i  29858  wl-sb8eut  30022  trer  30134  inixp  30219  notbinot1  30476  notbinot2  30480  truconj  30501  sbccom2lem  30529  sbccom2  30530  sbccom2f  30531  tsim1  30537  tsxo3  30546  tsxo4  30547  an43  30589  rmxypairf1o  30847  acsfn1p  31148  pm10.252  31266  pm10.253  31267  pm10.42  31269  aaanv  31294  pm13.195  31320  pm13.196a  31321  cncfshift  31676  dvnmul  31740  dvnprodlem2  31744  aibandbiaiffaiffb  32089  aovov0bi  32281  rexdifpr  32300  usgfislem1  32444  usgfisALTlem1  32448  copisnmnd  32497  pgrpgt2nabl  32959  lindslinindsimp2lem5  33063  islininds2  33085  ldepslinc  33110  sbc3or  33302  sbc3orgOLD  33303  en3lpVD  33645  3orbi123VD  33650  sbc3orgVD  33651  undif3VD  33682  ax6e2ndeqVD  33709  ax6e2ndeqALT  33731  sineq0ALT  33737  bnj115  33778  bnj156  33783  bnj206  33786  bnj110  33916  bnj121  33928  bnj124  33929  bnj130  33932  bnj153  33938  bnj207  33939  bnj581  33966  bnj611  33976  bnj864  33980  bnj865  33981  bnj893  33986  bnj1000  33999  bnj978  34007  bnj1040  34028  bnj1049  34030  bnj1133  34045  bnj1189  34065  bj-dfifc2  34164  bj-df-ifc  34165  bj-nf3  34197  bj-hbext  34264  bj-cleljust  34344  bj-denotes  34434  bj-ralcom4  34444  bj-rexcom4  34445  bj-elsngl  34526  bj-nuliotaALT  34587  isopos  34905  islvol5  35303  elpadd0  35533  dvhopellsm  36844  diblsmopel  36898  mapdvalc  37356  bj-ifim123g  37706  bj-ifidg  37707  bj-ifim1g  37714  bj-ifimimb  37715  bj-ifimim  37716  bj-ifnotnotb  37719  bj-ifororb  37726  bj-ifdfxor  37732  rp-fakeanorass  37737  rp-isfinite6  37744  cotr2g  37786  dfxor4  37789  dfhe3  37799  dffrege69  37959
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 185
  Copyright terms: Public domain W3C validator