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  785  anabs1  806  anabs7  808  pm4.76  861  pm5.63  915  jaoi2OLD  960  3ianor  982  3oran  984  pm3.2an3  1167  syl3anbr  1263  3an6  1300  nannot  1340  truan  1387  truimfal  1403  nottru  1406  nic-dfim  1477  nic-dfneg  1478  2nalexn  1620  2nexaln  1622  sbequ8  1707  dvelimf  2036  cleljust  2069  cleljustALT  2070  sb5rf  2130  sb6rf  2132  sb10f  2175  abeq1i  2583  nne  2654  necon3bbii  2714  necon2abii  2719  necon2bbii  2720  nabbiOLD  2787  nnel  2798  nnelOLD  2799  alexeq  3199  ceqsrexbv  3204  clel2  3206  clel4  3209  2reu5lem1  3275  2reu5lem2  3276  2reu5lem3  3277  dfsbcq2  3300  cbvreucsf  3435  nss  3528  raldifb  3610  difab  3733  un0  3776  in0  3777  ss0b  3781  ssunsn2  4149  iindif2  4356  nssss  4665  opthneg  4688  epse  4820  restidsing  5281  cotr  5329  issref  5330  mptpreima  5450  ralrnmpt  5975  fmptsng  6024  fmptsnd  6025  weniso  6176  uniuni  6518  suppvalbr  6828  eroveu  7329  isfinite2  7705  marypha1lem  7819  marypha2lem4  7824  wemapso2lem  7904  en3lplem2  7958  cantnfp1  8026  carden2  8294  fseqenlem1  8331  iscard3  8400  cardnum  8401  alephinit  8402  cardinfima  8404  alephiso  8405  dfac10b  8445  dfackm  8472  isfin5-2  8697  brdom7disj  8835  brdom6disj  8836  fsuppmapnn0fiubex  11955  hashtpg  12344  wrdeqswrdlsw  12501  wrd2ind  12530  splfv1  12555  cshwsexa  12616  s4f1o  12686  vdwapun  14193  cshwsiun  14284  cshwshash  14289  grpss  15718  pmtrfrn  16123  pmtrrn2  16125  pmtrprfvalrn  16153  issrg  16784  drngnidl  17487  drnglpir  17511  unocv  18298  dsmmacl  18359  pmatcollpw2lem  18849  toptopon  18937  ordtbas2  19194  ordtrest2  19207  restutopopn  20212  xmeterval  20406  ovolfcl  21349  eldv  21773  eltayl  22225  musumsum  22932  usgrafilem1  23793  trls  23904  is2wlk  23933  lejdii  25410  mdslle1i  26190  mdslle2i  26191  mdslj1i  26192  mdslj2i  26193  spc2ed  26326  mo5f  26337  unipreima  26428  2ndpreima  26469  xrge0infss  26520  ordtrest2NEW  26810  ordtconlem1  26811  ballotlem2  27327  plymulx0  27404  quad3  27759  relexpindlem  27797  fprod2dlem  27947  cnvco1  28026  cnvco2  28027  dfiota3  28410  nabi1i  28694  nabi2i  28695  wl-sb8eut  28858  trer  28971  inixp  29082  notbinot1  29339  impor  29341  notbinot2  29343  truconj  29364  sbcalf  29380  sbcexf  29381  exlimddvfi  29390  sbccom2lem  29393  sbccom2  29394  sbccom2f  29395  tsim1  29401  tsxo3  29410  tsxo4  29411  an43  29453  rmxypairf1o  29712  acsfn1p  30016  pm10.252  30073  pm10.253  30074  pm10.42  30076  aaanv  30101  pm13.195  30127  pm13.196a  30128  cncfshift  30441  fourierdlem80  30716  fourierswlem  30760  aibandbiaiffaiffb  30785  aovov0bi  30979  rexdifpr  31001  dff14a  31021  f13dfv  31024  rabasiun  31107  wwlknndef  31246  wlknwwlknvbij  31249  el2wlkonotot0  31268  usg2spthonot0  31285  clwwlknndef  31313  clwwlkvbij  31340  frgraun  31465  frgra2v  31468  4cycl2vnunb  31486  vdn0frgrav2  31493  vdgn0frgrav2  31494  2spotdisj  31531  usg2spot2nb  31535  usgreg2spot  31537  frgraregord013  31588  pgrpgt2nabel  31639  0rngnnzr  31646  lindslinindsimp2lem5  31768  islininds2  31790  ldepslinc  31823  fvmptnn04if  31847  sbc3or  32080  sbc3orgOLD  32081  en3lpVD  32424  3orbi123VD  32429  sbc3orgVD  32430  undif3VD  32461  ax6e2ndeqVD  32488  ax6e2ndeqALT  32510  sineq0ALT  32516  bnj115  32557  bnj156  32562  bnj206  32565  bnj110  32694  bnj121  32706  bnj124  32707  bnj130  32710  bnj153  32716  bnj207  32717  bnj581  32744  bnj611  32754  bnj864  32758  bnj865  32759  bnj893  32764  bnj1000  32777  bnj978  32785  bnj1040  32806  bnj1049  32808  bnj1133  32823  bnj1189  32843  bj-dfifc2  32944  bj-df-ifc  32945  bj-nf3  32979  bj-hbext  33045  bj-cleljust  33124  bj-denotes  33214  bj-ralcom4  33224  bj-rexcom4  33225  bj-elsngl  33306  bj-nuliotaALT  33367  isopos  33676  islvol5  34074  elpadd0  34304  dvhopellsm  35613  diblsmopel  35667  mapdvalc  36125  cotrgen  36473  bj-frege54cor0a  36561
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