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  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  2653  necon3bbii  2712  necon2abii  2717  necon2bbii  2718  nabbiOLD  2785  nnel  2796  nnelOLD  2797  alexeq  3194  ceqsrexbv  3199  clel2  3201  clel4  3204  2reu5lem1  3270  2reu5lem2  3271  2reu5lem3  3272  dfsbcq2  3295  cbvreucsf  3428  nss  3521  raldifb  3603  difab  3726  un0  3769  in0  3770  ss0b  3774  ssunsn2  4139  iindif2  4346  nssss  4655  opthneg  4678  epse  4810  restidsing  5269  cotr  5317  issref  5318  mptpreima  5438  ralrnmpt  5960  fmptsng  6008  weniso  6153  uniuni  6494  suppvalbr  6803  eroveu  7304  isfinite2  7680  marypha1lem  7793  marypha2lem4  7798  wemapso2lem  7877  en3lplem2  7931  cantnfp1  7999  carden2  8267  fseqenlem1  8304  iscard3  8373  cardnum  8374  alephinit  8375  cardinfima  8377  alephiso  8378  dfac10b  8418  dfackm  8445  isfin5-2  8670  brdom7disj  8808  brdom6disj  8809  hashtpg  12303  wrdeqswrdlsw  12460  wrd2ind  12489  splfv1  12514  cshwsexa  12575  s4f1o  12645  vdwapun  14152  cshwsiun  14243  cshwshash  14248  grpss  15677  pmtrfrn  16082  pmtrrn2  16084  pmtrprfvalrn  16112  issrg  16730  drngnidl  17433  drnglpir  17457  unocv  18229  dsmmacl  18290  toptopon  18669  ordtbas2  18926  ordtrest2  18939  restutopopn  19944  xmeterval  20138  ovolfcl  21081  eldv  21505  eltayl  21957  musumsum  22664  usgrafilem1  23475  trls  23586  is2wlk  23615  lejdii  25092  mdslle1i  25872  mdslle2i  25873  mdslj1i  25874  mdslj2i  25875  spc2ed  26008  mo5f  26019  unipreima  26111  2ndpreima  26152  xrge0infss  26203  ordtrest2NEW  26497  ordtconlem1  26498  ballotlem2  27014  plymulx0  27091  quad3  27446  relexpindlem  27484  fprod2dlem  27634  cnvco1  27713  cnvco2  27714  dfiota3  28097  nabi1i  28381  nabi2i  28382  wl-sb8eut  28545  trer  28658  inixp  28769  notbinot1  29026  impor  29028  notbinot2  29030  truconj  29051  sbcalf  29067  sbcexf  29068  exlimddvfi  29077  sbccom2lem  29080  sbccom2  29081  sbccom2f  29082  tsim1  29088  tsxo3  29097  tsxo4  29098  an43  29140  rmxypairf1o  29399  acsfn1p  29703  pm10.252  29760  pm10.253  29761  pm10.42  29763  aaanv  29788  pm13.195  29814  pm13.196a  29815  aibandbiaiffaiffb  30055  aovov0bi  30249  rexdifpr  30271  dff14a  30291  f13dfv  30294  rabasiun  30377  wwlknndef  30516  wlknwwlknvbij  30519  el2wlkonotot0  30538  usg2spthonot0  30555  clwwlknndef  30583  clwwlkvbij  30610  frgraun  30735  frgra2v  30738  4cycl2vnunb  30756  vdn0frgrav2  30763  vdgn0frgrav2  30764  2spotdisj  30801  usg2spot2nb  30805  usgreg2spot  30807  frgraregord013  30858  fmptsnd  30869  pgrpgt2nabel  30918  0rngnnzr  30925  fsuppmapnn0fiubex  30947  lindslinindsimp2lem5  31114  islininds2  31136  ldepslinc  31169  pmatcollpw2lem  31250  fvmptnn04if  31320  sbc3or  31554  sbc3orgOLD  31555  en3lpVD  31898  3orbi123VD  31903  sbc3orgVD  31904  undif3VD  31935  ax6e2ndeqVD  31962  ax6e2ndeqALT  31984  sineq0ALT  31990  bnj115  32031  bnj156  32036  bnj206  32039  bnj110  32168  bnj121  32180  bnj124  32181  bnj130  32184  bnj153  32190  bnj207  32191  bnj581  32218  bnj611  32228  bnj864  32232  bnj865  32233  bnj893  32238  bnj1000  32251  bnj978  32259  bnj1040  32280  bnj1049  32282  bnj1133  32297  bnj1189  32317  bj-dfifc2  32418  bj-df-ifc  32419  bj-nf3  32451  bj-hbext  32517  bj-cleljust  32596  bj-denotes  32686  bj-ralcom4  32696  bj-rexcom4  32697  bj-elsngl  32778  bj-nuliotaALT  32839  isopos  33148  islvol5  33546  elpadd0  33776  dvhopellsm  35085  diblsmopel  35139  mapdvalc  35597
  Copyright terms: Public domain W3C validator