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

Theorem bicomi 194
Description: Inference from commutative law for logical equivalence. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
bicomi.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
bicomi  |-  ( ps  <->  ph )

Proof of Theorem bicomi
StepHypRef Expression
1 bicomi.1 . 2  |-  ( ph  <->  ps )
2 bicom1 191 . 2  |-  ( (
ph 
<->  ps )  ->  ( ps 
<-> 
ph ) )
31, 2ax-mp 8 1  |-  ( ps  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 177
This theorem is referenced by:  biimpri  198  bitr2i  242  bitr3i  243  bitr4i  244  syl5bbr  251  syl5rbbr  252  syl6bbr  255  syl6rbbr  256  mtbir  291  sylnibr  297  sylnbir  299  xchnxbir  301  xchbinxr  303  con1bii  322  con2bii  323  nbn  337  xor3  347  pm5.41  354  pm4.64  362  pm4.63  411  pm4.61  416  anor  476  pm4.53  479  pm4.55  481  pm4.56  482  pm4.57  484  pm4.25  502  pm4.87  568  anidm  626  pm4.77  763  anabs1  784  anabs7  786  pm4.76  837  pm5.63  891  jaoi2  934  3ianor  951  3oran  953  pm3.2an3  1133  syl3anbr  1228  3an6  1264  nannot  1299  truimfal  1351  nottru  1354  nic-dfim  1440  nic-dfneg  1441  2nalexn  1579  sbid  1936  dvelimf  2031  cleljust  2048  cleljustALT  2049  sb10f  2156  nne  2554  necon3bbii  2581  necon2abii  2605  necon2bbii  2606  nnel  2648  alexeq  3008  ceqsrexbv  3013  clel2  3015  clel4  3018  2reu5lem1  3082  2reu5lem2  3083  2reu5lem3  3084  dfsbcq2  3107  cbvreucsf  3256  nss  3349  raldifb  3430  difab  3553  un0  3595  in0  3596  ss0b  3600  ssunsn2  3901  iindif2  4101  nssss  4360  epse  4506  uniuni  4656  cotr  5186  issref  5187  mptpreima  5303  ralrnmpt  5817  weniso  6014  eroveu  6935  isfinite2  7301  marypha1lem  7373  marypha2lem4  7378  en3lplem2  7604  carden2  7807  fseqenlem1  7838  iscard3  7907  cardnum  7908  alephinit  7909  cardinfima  7911  alephiso  7912  dfac10b  7952  dfackm  7979  isfin5-2  8204  brdom7disj  8342  brdom6disj  8343  hashtpg  11618  splfv1  11711  s4f1o  11792  vdwapun  13269  grpss  14753  drngnidl  16227  drnglpir  16251  unocv  16830  toptopon  16921  ordtbas2  17177  ordtrest2  17190  restutopopn  18189  xmeterval  18352  ovolfcl  19230  eldv  19652  eltayl  20143  musumsum  20844  usgrafilem1  21291  trls  21400  lejdii  22888  mdslle1i  23668  mdslle2i  23669  mdslj1i  23670  mdslj2i  23671  mo5f  23816  unipreima  23898  2ndpreima  23937  ballotlem2  24525  relexpindlem  24918  cnvco1  25141  cnvco2  25142  dfiota3  25486  nabi1i  25855  nabi2i  25856  itgaddnclem2  25964  trer  26010  inixp  26121  an43  26386  rmxypairf1o  26665  dsmmacl  26876  pmtrfrn  27069  acsfn1p  27176  pm10.252  27225  pm10.253  27226  pm10.42  27228  2nexaln  27242  aaanv  27256  pm13.195  27282  pm13.196a  27283  aibandbiaiffaiffb  27530  aovov0bi  27729  frgraun  27749  4cycl2vnunb  27770  vdn0frgrav2  27777  vdgn0frgrav2  27778  sbc3org  27959  en3lpVD  28298  3orbi123VD  28303  sbc3orgVD  28304  undif3VD  28335  a9e2ndeqVD  28362  a9e2ndeqALT  28385  bnj115  28428  bnj156  28433  bnj206  28436  bnj110  28567  bnj121  28579  bnj124  28580  bnj130  28583  bnj153  28589  bnj207  28590  bnj581  28617  bnj611  28627  bnj864  28631  bnj865  28632  bnj893  28637  bnj1000  28650  bnj978  28658  bnj1040  28679  bnj1049  28681  bnj1133  28696  bnj1189  28716  cleljustNEW7  28960  dvelimfOLD7  29043  sb10fOLD7  29083  isopos  29295  islvol5  29693  elpadd0  29923  dvhopellsm  31232  diblsmopel  31286  mapdvalc  31744
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator