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

Theorem bicomi 193
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 190 . 2  |-  ( (
ph 
<->  ps )  ->  ( ps 
<-> 
ph ) )
31, 2ax-mp 8 1  |-  ( ps  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 176
This theorem is referenced by:  biimpri  197  bitr2i  241  bitr3i  242  bitr4i  243  syl5bbr  250  syl5rbbr  251  syl6bbr  254  syl6rbbr  255  mtbir  290  sylnibr  296  sylnbir  298  xchnxbir  300  xchbinxr  302  con1bii  321  con2bii  322  nbn  336  xor3  346  pm5.41  353  pm4.64  361  pm4.63  410  pm4.61  415  anor  475  pm4.53  478  pm4.55  480  pm4.56  481  pm4.57  483  pm4.25  501  pm4.87  567  anidm  625  pm4.77  762  anabs1  783  anabs7  785  pm4.76  836  pm5.63  890  3ianor  949  3oran  951  pm3.2an3  1131  syl3anbr  1226  3an6  1262  nannot  1293  truimfal  1335  nottru  1338  nic-dfim  1424  nic-dfneg  1425  2nalexn  1560  sbid  1863  dvelimf  1937  cleljust  1954  cleljustALT  1955  sb10f  2061  nne  2450  necon3bbii  2477  necon2abii  2501  necon2bbii  2502  alexeq  2897  ceqsrexbv  2902  clel2  2904  clel4  2907  2reu5lem1  2970  2reu5lem2  2971  2reu5lem3  2972  dfsbcq2  2994  cbvreucsf  3145  nss  3236  difab  3437  un0  3479  in0  3480  ss0b  3484  ssunsn2  3773  iindif2  3971  nssss  4229  epse  4376  uniuni  4527  reusv2lem4  4538  cotr  5055  issref  5056  mptpreima  5166  ralrnmpt  5669  weniso  5852  eroveu  6753  isfinite2  7115  marypha1lem  7186  marypha2lem4  7191  en3lplem2  7417  carden2  7620  fseqenlem1  7651  iscard3  7720  cardnum  7721  alephinit  7722  cardinfima  7724  alephiso  7725  dfac10b  7765  dfackm  7792  isfin5-2  8017  brdom7disj  8156  brdom6disj  8157  splfv1  11470  vdwapun  13021  grpss  14503  drngnidl  15981  drnglpir  16005  unocv  16580  toptopon  16671  ordtbas2  16921  ordtrest2  16934  xmeterval  17978  ovolfcl  18826  eldv  19248  eltayl  19739  musumsum  20432  lejdii  22117  mdslle1i  22897  mdslle2i  22898  mdslj1i  22899  mdslj2i  22900  ballotlem2  23047  relexpindlem  23447  cnvco1  23528  cnvco2  23529  elfuns  23865  dfiota3  23873  funpartfv  23894  nabi1i  24241  nabi2i  24242  negcmpprcal2  24358  eqvinopb  24377  boxeq  24399  notev  24402  notal  24403  albineal  24411  splint  24460  restidsing  24488  imfstnrelc  24493  defse3  24684  qusp  24954  algi  25139  prismorcsetlemc  25329  nbssntrs  25559  trer  25639  inixp  25811  an43  26124  rmxypairf1o  26408  dsmmacl  26619  pmtrfrn  26812  acsfn1p  26919  pm10.252  26968  pm10.253  26969  pm10.42  26971  2nexaln  26985  aaanv  26999  pm13.195  27025  pm13.196a  27026  rfcnnnub  27119  aovov0bi  27468  f1oun2prg  27487  s4f1o  27492  frgra3v  27542  sbc3org  27668  en3lpVD  27994  3orbi123VD  27999  sbc3orgVD  28000  undif3VD  28031  a9e2ndeqVD  28058  a9e2ndeqALT  28081  bnj115  28124  bnj156  28129  bnj206  28132  bnj110  28263  bnj121  28275  bnj124  28276  bnj130  28279  bnj153  28285  bnj207  28286  bnj605  28312  bnj581  28313  bnj611  28323  bnj864  28327  bnj865  28328  bnj893  28333  bnj1000  28346  bnj978  28354  bnj1040  28375  bnj1049  28377  bnj1133  28392  bnj1189  28412  isopos  28743  islvol5  29141  elpadd0  29371  dvhopellsm  30680  diblsmopel  30734  mapdvalc  31192
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 177
  Copyright terms: Public domain W3C validator