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  1302  truimfal  1354  nottru  1357  nic-dfim  1443  nic-dfneg  1444  2nalexn  1582  sbid  1947  dvelimf  2064  dvelimfOLD  2065  cleljust  2097  cleljustALT  2098  sb10f  2198  nne  2597  necon3bbii  2624  necon2abii  2648  necon2bbii  2649  nnel  2691  alexeq  3052  ceqsrexbv  3057  clel2  3059  clel4  3062  2reu5lem1  3126  2reu5lem2  3127  2reu5lem3  3128  dfsbcq2  3151  cbvreucsf  3300  nss  3393  raldifb  3474  difab  3597  un0  3639  in0  3640  ss0b  3644  ssunsn2  3945  iindif2  4147  nssss  4406  epse  4552  uniuni  4702  cotr  5232  issref  5233  mptpreima  5349  ralrnmpt  5864  weniso  6061  eroveu  6985  isfinite2  7351  marypha1lem  7424  marypha2lem4  7429  en3lplem2  7655  carden2  7858  fseqenlem1  7889  iscard3  7958  cardnum  7959  alephinit  7960  cardinfima  7962  alephiso  7963  dfac10b  8003  dfackm  8030  isfin5-2  8255  brdom7disj  8393  brdom6disj  8394  hashtpg  11674  splfv1  11767  s4f1o  11848  vdwapun  13325  grpss  14809  drngnidl  16283  drnglpir  16307  unocv  16890  toptopon  16981  ordtbas2  17238  ordtrest2  17251  restutopopn  18251  xmeterval  18445  ovolfcl  19346  eldv  19768  eltayl  20259  musumsum  20960  usgrafilem1  21408  trls  21519  is2wlk  21548  lejdii  23023  mdslle1i  23803  mdslle2i  23804  mdslj1i  23805  mdslj2i  23806  mo5f  23955  unipreima  24039  2ndpreima  24079  ballotlem2  24729  relexpindlem  25122  fprod2dlem  25288  cnvco1  25367  cnvco2  25368  dfiota3  25713  nabi1i  26084  nabi2i  26085  trer  26251  inixp  26362  an43  26627  rmxypairf1o  26906  dsmmacl  27117  pmtrfrn  27310  acsfn1p  27417  pm10.252  27466  pm10.253  27467  pm10.42  27469  2nexaln  27483  aaanv  27497  pm13.195  27523  pm13.196a  27524  aibandbiaiffaiffb  27771  aovov0bi  27969  rexdifpr  27989  dff14a  28001  f13dfv  28004  el2wlkonotot0  28111  usg2spthonot0  28128  frgraun  28142  4cycl2vnunb  28163  vdn0frgrav2  28170  vdgn0frgrav2  28171  2spotdisj  28206  usg2spot2nb  28210  usgreg2spot  28212  sbc3org  28369  en3lpVD  28709  3orbi123VD  28714  sbc3orgVD  28715  undif3VD  28746  a9e2ndeqVD  28773  a9e2ndeqALT  28796  bnj115  28842  bnj156  28847  bnj206  28850  bnj110  28981  bnj121  28993  bnj124  28994  bnj130  28997  bnj153  29003  bnj207  29004  bnj581  29031  bnj611  29041  bnj864  29045  bnj865  29046  bnj893  29051  bnj1000  29064  bnj978  29072  bnj1040  29093  bnj1049  29095  bnj1133  29110  bnj1189  29130  cleljustNEW7  29374  dvelimfOLD7  29457  sb10fOLD7  29497  isopos  29709  islvol5  30107  elpadd0  30337  dvhopellsm  31646  diblsmopel  31700  mapdvalc  32158
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