MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bicomi 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 10 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  3ianor  951  3oran  953  pm3.2an3  1133  syl3anbr  1228  3an6  1264  nannot  1295  truimfal  1337  nottru  1340  nic-dfim  1425  nic-dfneg  1426  2nalexn  1561  sbid  1864  dvelimf  1941  cleljust  1959  cleljustALT  1960  sb10f  2064  nne  2451  necon3bbii  2478  necon2abii  2502  necon2bbii  2503  alexeq  2898  ceqsrexbv  2903  clel2  2905  clel4  2908  2reu5lem1  2971  2reu5lem2  2972  2reu5lem3  2973  dfsbcq2  2995  cbvreucsf  3146  nss  3237  difab  3438  un0  3480  in0  3481  ss0b  3485  ssunsn2  3774  iindif2  3972  nssss  4228  epse  4375  uniuni  4526  reusv2lem4  4537  cotr  5054  issref  5055  mptpreima  5164  ralrnmpt  5630  weniso  5813  eroveu  6748  isfinite2  7110  marypha1lem  7181  marypha2lem4  7186  en3lplem2  7412  carden2  7615  fseqenlem1  7646  iscard3  7715  cardnum  7716  alephinit  7717  cardinfima  7719  alephiso  7720  dfac10b  7760  dfackm  7787  isfin5-2  8012  brdom7disj  8151  brdom6disj  8152  splfv1  11464  vdwapun  13015  grpss  14497  drngnidl  15975  drnglpir  15999  unocv  16574  toptopon  16665  ordtbas2  16915  ordtrest2  16928  xmeterval  17972  ovolfcl  18820  eldv  19242  eltayl  19733  musumsum  20426  lejdii  22109  mdslle1i  22889  mdslle2i  22890  mdslj1i  22891  mdslj2i  22892  ballotlem2  23040  relexpindlem  23440  cnvco1  23520  cnvco2  23521  dfiota3  23869  funpartfv  23890  nabi1i  24237  nabi2i  24238  negcmpprcal2  24344  eqvinopb  24363  boxeq  24385  notev  24388  notal  24389  albineal  24397  splint  24446  restidsing  24474  imfstnrelc  24479  defse3  24671  qusp  24941  algi  25126  prismorcsetlemc  25316  nbssntrs  25546  trer  25626  inixp  25798  an43  26111  rmxypairf1o  26395  dsmmacl  26606  pmtrfrn  26799  acsfn1p  26906  pm10.252  26955  pm10.253  26956  pm10.42  26958  2nexaln  26972  aaanv  26986  pm13.195  27012  pm13.196a  27013  rfcnnnub  27106  aovov0bi  27435  sbc3org  27566  en3lpVD  27889  3orbi123VD  27894  sbc3orgVD  27895  undif3VD  27926  a9e2ndeqVD  27953  a9e2ndeqALT  27976  bnj115  28018  bnj156  28023  bnj206  28026  bnj110  28157  bnj121  28169  bnj124  28170  bnj130  28173  bnj153  28179  bnj207  28180  bnj605  28206  bnj581  28207  bnj611  28217  bnj864  28221  bnj865  28222  bnj893  28227  bnj1000  28240  bnj978  28248  bnj1040  28269  bnj1049  28271  bnj1133  28286  bnj1189  28306  isopos  28637  islvol5  29035  elpadd0  29265  dvhopellsm  30574  diblsmopel  30628  mapdvalc  31086
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator