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  1563  sbid  1875  dvelimf  1950  cleljust  1967  cleljustALT  1968  sb10f  2074  nne  2463  necon3bbii  2490  necon2abii  2514  necon2bbii  2515  alexeq  2910  ceqsrexbv  2915  clel2  2917  clel4  2920  2reu5lem1  2983  2reu5lem2  2984  2reu5lem3  2985  dfsbcq2  3007  cbvreucsf  3158  nss  3249  difab  3450  un0  3492  in0  3493  ss0b  3497  ssunsn2  3789  iindif2  3987  nssss  4245  epse  4392  uniuni  4543  reusv2lem4  4554  cotr  5071  issref  5072  mptpreima  5182  ralrnmpt  5685  weniso  5868  eroveu  6769  isfinite2  7131  marypha1lem  7202  marypha2lem4  7207  en3lplem2  7433  carden2  7636  fseqenlem1  7667  iscard3  7736  cardnum  7737  alephinit  7738  cardinfima  7740  alephiso  7741  dfac10b  7781  dfackm  7808  isfin5-2  8033  brdom7disj  8172  brdom6disj  8173  splfv1  11486  vdwapun  13037  grpss  14519  drngnidl  15997  drnglpir  16021  unocv  16596  toptopon  16687  ordtbas2  16937  ordtrest2  16950  xmeterval  17994  ovolfcl  18842  eldv  19264  eltayl  19755  musumsum  20448  lejdii  22133  mdslle1i  22913  mdslle2i  22914  mdslj1i  22915  mdslj2i  22916  ballotlem2  23063  mo5f  23159  disjex  23192  unipreima  23224  relexpindlem  24051  cnvco1  24188  cnvco2  24189  elfuns  24525  dfiota3  24533  funpartlem  24552  nabi1i  24902  nabi2i  24903  itgaddnclem2  25010  negcmpprcal2  25049  eqvinopb  25068  boxeq  25090  notev  25093  notal  25094  albineal  25102  splint  25151  restidsing  25179  imfstnrelc  25184  defse3  25375  qusp  25645  algi  25830  prismorcsetlemc  26020  nbssntrs  26250  trer  26330  inixp  26502  an43  26815  rmxypairf1o  27099  dsmmacl  27310  pmtrfrn  27503  acsfn1p  27610  pm10.252  27659  pm10.253  27660  pm10.42  27662  2nexaln  27676  aaanv  27690  pm13.195  27716  pm13.196a  27717  rfcnnnub  27810  aovov0bi  28164  jaoi2  28176  f1oun2prg  28187  hashtpg  28217  s4f1o  28225  nbgranself2  28285  trls  28335  frgra3v  28426  4cycl2vnunb  28439  sbc3org  28594  en3lpVD  28937  3orbi123VD  28942  sbc3orgVD  28943  undif3VD  28974  a9e2ndeqVD  29001  a9e2ndeqALT  29024  bnj115  29067  bnj156  29072  bnj206  29075  bnj110  29206  bnj121  29218  bnj124  29219  bnj130  29222  bnj153  29228  bnj207  29229  bnj605  29255  bnj581  29256  bnj611  29266  bnj864  29270  bnj865  29271  bnj893  29276  bnj1000  29289  bnj978  29297  bnj1040  29318  bnj1049  29320  bnj1133  29335  bnj1189  29355  cleljustNEW7  29599  cleljustALTNEW7  29600  dvelimfOLD7  29681  sb10fOLD7  29722  isopos  29992  islvol5  30390  elpadd0  30620  dvhopellsm  31929  diblsmopel  31983  mapdvalc  32441
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