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

Theorem bicomi 202
Description: Inference from commutative law for logical equivalence. (Contributed by NM, 3-Jan-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 199 . 2  |-  ( (
ph 
<->  ps )  ->  ( ps 
<-> 
ph ) )
31, 2ax-mp 5 1  |-  ( ps  <->  ph )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184
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
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  864  pm5.63  922  jaoi2OLD  967  3ianor  990  3oran  992  pm3.2an3  1175  syl3anbr  1272  3an6  1309  nannot  1349  truan  1396  truimfal  1412  nottru  1415  nic-dfim  1486  nic-dfneg  1487  2nalexn  1629  2nexaln  1631  sbequ8  1716  dvelimf  2049  cleljust  2082  cleljustALT  2083  sb5rf  2143  sb6rf  2145  sb10f  2188  abeq1i  2596  nne  2668  necon3bbii  2728  necon2abii  2733  necon2bbii  2734  nabbiOLD  2801  nnel  2812  nnelOLD  2813  alexeq  3233  ceqsrexbv  3238  clel2  3240  clel4  3243  2reu5lem1  3309  2reu5lem2  3310  2reu5lem3  3311  dfsbcq2  3334  cbvreucsf  3469  nss  3562  raldifb  3644  difab  3767  un0  3810  in0  3811  ss0b  3815  ssunsn2  4186  rabasiun  4329  iindif2  4394  nssss  4703  opthneg  4726  epse  4862  restidsing  5330  cotrg  5378  issref  5380  mptpreima  5500  ralrnmpt  6030  fmptsng  6082  fmptsnd  6083  dff14a  6165  f13dfv  6168  weniso  6238  uniuni  6593  suppvalbr  6905  eroveu  7406  isfinite2  7778  marypha1lem  7893  marypha2lem4  7898  wemapso2lem  7978  en3lplem2  8032  cantnfp1  8100  carden2  8368  fseqenlem1  8405  iscard3  8474  cardnum  8475  alephinit  8476  cardinfima  8478  alephiso  8479  dfac10b  8519  dfackm  8546  isfin5-2  8771  brdom7disj  8909  brdom6disj  8910  fsuppmapnn0fiubex  12066  hashtpg  12489  wrdeqswrdlsw  12637  wrd2ind  12666  splfv1  12694  cshwsexa  12755  s4f1o  12829  vdwapun  14351  cshwsiun  14442  cshwshash  14447  grpss  15881  pmtrfrn  16289  pmtrrn2  16291  pmtrprfvalrn  16319  issrg  16961  drngnidl  17676  drnglpir  17700  0rngnnzr  17716  unocv  18506  dsmmacl  18567  pmatcollpw2lem  19073  fvmptnn04if  19145  toptopon  19229  ordtbas2  19486  ordtrest2  19499  restutopopn  20504  xmeterval  20698  ovolfcl  21641  eldv  22065  eltayl  22517  musumsum  23224  usgrafilem1  24115  trls  24242  is2wlk  24271  wwlknndef  24441  wlknwwlknvbij  24444  clwwlknndef  24477  clwwlkvbij  24505  el2wlkonotot0  24576  usg2spthonot0  24593  frgraun  24700  frgra2v  24703  4cycl2vnunb  24721  vdn0frgrav2  24728  vdgn0frgrav2  24729  2spotdisj  24766  usg2spot2nb  24770  usgreg2spot  24772  frgraregord013  24823  lejdii  26160  mdslle1i  26940  mdslle2i  26941  mdslj1i  26942  mdslj2i  26943  spc2ed  27076  mo5f  27087  unipreima  27184  2ndpreima  27225  xrge0infss  27276  ordtrest2NEW  27569  ordtconlem1  27570  ballotlem2  28095  plymulx0  28172  quad3  28527  relexpindlem  28565  fprod2dlem  28715  cnvco1  28794  cnvco2  28795  dfiota3  29178  nabi1i  29462  nabi2i  29463  wl-sb8eut  29627  trer  29739  inixp  29850  notbinot1  30107  impor  30109  notbinot2  30111  truconj  30132  sbcalf  30148  sbcexf  30149  exlimddvfi  30158  sbccom2lem  30161  sbccom2  30162  sbccom2f  30163  tsim1  30169  tsxo3  30178  tsxo4  30179  an43  30221  rmxypairf1o  30479  acsfn1p  30781  pm10.252  30872  pm10.253  30873  pm10.42  30875  aaanv  30900  pm13.195  30926  pm13.196a  30927  cncfshift  31240  fourierdlem80  31515  fourierswlem  31559  aibandbiaiffaiffb  31584  aovov0bi  31776  rexdifpr  31795  usgfislem1  31939  usgfisALTlem1  31943  pgrpgt2nabl  32056  lindslinindsimp2lem5  32162  islininds2  32184  ldepslinc  32209  sbc3or  32399  sbc3orgOLD  32400  en3lpVD  32743  3orbi123VD  32748  sbc3orgVD  32749  undif3VD  32780  ax6e2ndeqVD  32807  ax6e2ndeqALT  32829  sineq0ALT  32835  bnj115  32876  bnj156  32881  bnj206  32884  bnj110  33013  bnj121  33025  bnj124  33026  bnj130  33029  bnj153  33035  bnj207  33036  bnj581  33063  bnj611  33073  bnj864  33077  bnj865  33078  bnj893  33083  bnj1000  33096  bnj978  33104  bnj1040  33125  bnj1049  33127  bnj1133  33142  bnj1189  33162  bj-dfifc2  33263  bj-df-ifc  33264  bj-nf3  33298  bj-hbext  33364  bj-cleljust  33443  bj-denotes  33533  bj-ralcom4  33543  bj-rexcom4  33544  bj-elsngl  33625  bj-nuliotaALT  33686  isopos  33995  islvol5  34393  elpadd0  34623  dvhopellsm  35932  diblsmopel  35986  mapdvalc  36444  bj-frege54cor0a  36890
  Copyright terms: Public domain W3C validator