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  787  anabs1  808  anabs7  810  pm4.76  866  pm5.63  924  3ianor  991  3oran  993  pm3.2an3  1176  syl3anbr  1273  3an6  1310  nannot  1352  nanbi  1353  truan  1400  truimfal  1416  nottru  1419  nic-dfim  1489  nic-dfneg  1490  2nalexn  1636  2nexaln  1638  sbequ8  1731  dvelimf  2062  cleljust  2095  cleljustALT  2096  sb5rf  2151  sb6rf  2152  sb10f  2186  abeq1i  2572  nne  2644  necon3bbii  2704  necon2abii  2709  necon2bbii  2710  nabbiOLD  2777  nnel  2788  nnelOLD  2789  alexeq  3215  ceqsrexbv  3220  clel2  3222  clel4  3225  2reu5lem1  3291  2reu5lem2  3292  2reu5lem3  3293  dfsbcq2  3316  cbvreucsf  3454  nss  3547  raldifb  3629  difab  3752  un0  3796  in0  3797  ss0b  3801  ssunsn2  4174  rabasiun  4319  iindif2  4384  nssss  4693  opthneg  4716  epse  4852  restidsing  5320  cotrg  5368  issref  5370  mptpreima  5490  ralrnmpt  6025  fmptsng  6077  fmptsnd  6078  dff14a  6162  f13dfv  6165  weniso  6235  uniuni  6594  suppvalbr  6907  eroveu  7408  isfinite2  7780  marypha1lem  7895  marypha2lem4  7900  wemapso2lem  7981  en3lplem2  8035  cantnfp1  8103  carden2  8371  fseqenlem1  8408  iscard3  8477  cardnum  8478  alephinit  8479  cardinfima  8481  alephiso  8482  dfac10b  8522  dfackm  8549  isfin5-2  8774  brdom7disj  8912  brdom6disj  8913  fsuppmapnn0fiubex  12077  hashtpg  12502  wrdeqswrdlsw  12653  wrd2ind  12682  splfv1  12710  cshwsexa  12771  s4f1o  12845  vdwapun  14369  cshwsiun  14461  cshwshash  14466  grpss  15945  pmtrfrn  16357  pmtrrn2  16359  pmtrprfvalrn  16387  issrg  17033  drngnidl  17751  drnglpir  17775  0ringnnzr  17791  unocv  18584  dsmmacl  18645  pmatcollpw2lem  19151  fvmptnn04if  19223  toptopon  19307  ordtbas2  19565  ordtrest2  19578  xmeterval  20808  ovolfcl  21751  eldv  22175  eltayl  22627  musumsum  23340  usgrafilem1  24283  trls  24410  is2wlk  24439  wwlknndef  24609  wlknwwlknvbij  24612  clwwlknndef  24645  clwwlkvbij  24673  el2wlkonotot0  24744  usg2spthonot0  24761  frgraun  24868  frgra2v  24871  4cycl2vnunb  24889  vdn0frgrav2  24895  vdgn0frgrav2  24896  2spotdisj  24933  usg2spot2nb  24937  usgreg2spot  24939  frgraregord013  24990  lejdii  26328  mdslle1i  27108  mdslle2i  27109  mdslj1i  27110  mdslj2i  27111  mo5f  27255  unipreima  27356  2ndpreima  27397  xrge0infss  27452  ordtrest2NEW  27778  ordtconlem1  27779  ballotlem2  28300  plymulx0  28377  relexpindlem  28935  cnvco1  29164  cnvco2  29165  dfiota3  29548  nabi1i  29832  nabi2i  29833  wl-sb8eut  29997  trer  30109  inixp  30194  notbinot1  30451  notbinot2  30455  truconj  30476  sbccom2lem  30504  sbccom2  30505  sbccom2f  30506  tsim1  30512  tsxo3  30521  tsxo4  30522  an43  30564  rmxypairf1o  30822  acsfn1p  31124  pm10.252  31220  pm10.253  31221  pm10.42  31223  aaanv  31248  pm13.195  31274  pm13.196a  31275  cncfshift  31583  aibandbiaiffaiffb  31927  aovov0bi  32119  rexdifpr  32138  usgfislem1  32282  usgfisALTlem1  32286  copisnmnd  32334  pgrpgt2nabl  32687  lindslinindsimp2lem5  32793  islininds2  32815  ldepslinc  32840  sbc3or  33030  sbc3orgOLD  33031  en3lpVD  33373  3orbi123VD  33378  sbc3orgVD  33379  undif3VD  33410  ax6e2ndeqVD  33437  ax6e2ndeqALT  33459  sineq0ALT  33465  bnj115  33506  bnj156  33511  bnj206  33514  bnj110  33644  bnj121  33656  bnj124  33657  bnj130  33660  bnj153  33666  bnj207  33667  bnj581  33694  bnj611  33704  bnj864  33708  bnj865  33709  bnj893  33714  bnj1000  33727  bnj978  33735  bnj1040  33756  bnj1049  33758  bnj1133  33773  bnj1189  33793  bj-dfifc2  33906  bj-df-ifc  33907  bj-nf3  33939  bj-hbext  34006  bj-cleljust  34086  bj-denotes  34176  bj-ralcom4  34186  bj-rexcom4  34187  bj-elsngl  34268  bj-nuliotaALT  34329  isopos  34639  islvol5  35037  elpadd0  35267  dvhopellsm  36578  diblsmopel  36632  mapdvalc  37090  rp-fakeanorass  37434  rp-isfinite6  37441  cotr2g  37473  dfhe3  37480  dffrege69  37622
  Copyright terms: Public domain W3C validator