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

Theorem bicomi 195
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 192 . 2  |-  ( (
ph 
<->  ps )  ->  ( ps 
<-> 
ph ) )
31, 2ax-mp 5 1  |-  ( ps  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 178
This theorem is referenced by:  biimpri  199  bitr2i  243  bitr3i  244  bitr4i  245  syl5bbr  252  syl5rbbr  253  syl6bbr  256  syl6rbbr  257  mtbir  292  sylnibr  298  sylnbir  300  xchnxbir  302  xchbinxr  304  con1bii  323  con2bii  324  nbn  338  xor3  348  pm5.41  355  pm4.64  363  pm4.63  412  pm4.61  417  anor  477  pm4.53  480  pm4.55  482  pm4.56  483  pm4.57  485  pm4.25  503  pm4.87  569  anidm  627  pm4.77  764  anabs1  785  anabs7  787  pm4.76  838  pm5.63  892  jaoi2  935  3ianor  952  3oran  954  pm3.2an3  1134  syl3anbr  1229  3an6  1265  nannot  1303  truimfal  1355  nottru  1358  nic-dfim  1444  nic-dfneg  1445  2nalexn  1583  sbequ8  1665  sbid  1950  dvelimf  2071  dvelimfOLD  2072  cleljust  2107  cleljustALT  2108  sb10f  2205  nne  2611  necon3bbii  2638  necon2abii  2665  necon2bbii  2666  nnel  2710  alexeq  3071  ceqsrexbv  3076  clel2  3078  clel4  3081  2reu5lem1  3145  2reu5lem2  3146  2reu5lem3  3147  dfsbcq2  3170  cbvreucsf  3299  nss  3392  raldifb  3473  difab  3595  un0  3637  in0  3638  ss0b  3642  ssunsn2  3982  iindif2  4184  nssss  4448  epse  4594  uniuni  4745  cotr  5275  issref  5276  mptpreima  5392  ralrnmpt  5907  weniso  6104  eroveu  7028  isfinite2  7394  marypha1lem  7467  marypha2lem4  7472  en3lplem2  7700  carden2  7905  fseqenlem1  7936  iscard3  8005  cardnum  8006  alephinit  8007  cardinfima  8009  alephiso  8010  dfac10b  8050  dfackm  8077  isfin5-2  8302  brdom7disj  8440  brdom6disj  8441  hashtpg  11722  splfv1  11815  s4f1o  11896  vdwapun  13373  grpss  14857  drngnidl  16331  drnglpir  16355  unocv  16938  toptopon  17029  ordtbas2  17286  ordtrest2  17299  restutopopn  18299  xmeterval  18493  ovolfcl  19394  eldv  19816  eltayl  20307  musumsum  21008  usgrafilem1  21456  trls  21567  is2wlk  21596  lejdii  23071  mdslle1i  23851  mdslle2i  23852  mdslj1i  23853  mdslj2i  23854  mo5f  24003  unipreima  24087  2ndpreima  24127  ballotlem2  24777  relexpindlem  25170  fprod2dlem  25335  cnvco1  25414  cnvco2  25415  dfiota3  25799  nabi1i  26172  nabi2i  26173  trer  26357  inixp  26468  an43  26733  rmxypairf1o  27012  dsmmacl  27222  pmtrfrn  27415  acsfn1p  27522  pm10.252  27571  pm10.253  27572  pm10.42  27574  2nexaln  27588  aaanv  27602  pm13.195  27628  pm13.196a  27629  aibandbiaiffaiffb  27876  aovov0bi  28074  rexdifpr  28097  dff14a  28120  f13dfv  28123  cshwsiun  28344  cshwssize  28348  cshwsexa  28349  el2wlkonotot0  28428  usg2spthonot0  28445  frgraun  28484  4cycl2vnunb  28505  vdn0frgrav2  28512  vdgn0frgrav2  28513  2spotdisj  28548  usg2spot2nb  28552  usgreg2spot  28554  sbc3org  28714  en3lpVD  29055  3orbi123VD  29060  sbc3orgVD  29061  undif3VD  29092  a9e2ndeqVD  29119  a9e2ndeqALT  29141  sineq0ALT  29147  bnj115  29188  bnj156  29193  bnj206  29196  bnj110  29327  bnj121  29339  bnj124  29340  bnj130  29343  bnj153  29349  bnj207  29350  bnj581  29377  bnj611  29387  bnj864  29391  bnj865  29392  bnj893  29397  bnj1000  29410  bnj978  29418  bnj1040  29439  bnj1049  29441  bnj1133  29456  bnj1189  29476  cleljustNEW7  29725  dvelimfOLD7  29825  sb10fOLD7  29864  isopos  30076  islvol5  30474  elpadd0  30704  dvhopellsm  32013  diblsmopel  32067  mapdvalc  32525
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 179
  Copyright terms: Public domain W3C validator