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  1345  nottru  1348  nic-dfim  1434  nic-dfneg  1435  2nalexn  1573  sbid  1927  dvelimf  2002  cleljust  2019  cleljustALT  2020  sb10f  2127  nne  2525  necon3bbii  2552  necon2abii  2576  necon2bbii  2577  alexeq  2973  ceqsrexbv  2978  clel2  2980  clel4  2983  2reu5lem1  3046  2reu5lem2  3047  2reu5lem3  3048  dfsbcq2  3070  cbvreucsf  3221  nss  3312  difab  3513  un0  3555  in0  3556  ss0b  3560  ssunsn2  3854  iindif2  4052  nssss  4311  epse  4458  uniuni  4609  reusv2lem4  4620  cotr  5137  issref  5138  mptpreima  5248  ralrnmpt  5752  weniso  5939  eroveu  6841  isfinite2  7205  marypha1lem  7276  marypha2lem4  7281  en3lplem2  7507  carden2  7710  fseqenlem1  7741  iscard3  7810  cardnum  7811  alephinit  7812  cardinfima  7814  alephiso  7815  dfac10b  7855  dfackm  7882  isfin5-2  8107  brdom7disj  8246  brdom6disj  8247  splfv1  11566  vdwapun  13118  grpss  14602  drngnidl  16080  drnglpir  16104  unocv  16686  toptopon  16777  ordtbas2  17027  ordtrest2  17040  xmeterval  18080  ovolfcl  18930  eldv  19352  eltayl  19843  musumsum  20544  lejdii  22231  mdslle1i  23011  mdslle2i  23012  mdslj1i  23013  mdslj2i  23014  mo5f  23167  disjex  23230  unipreima  23259  2ndpreima  23300  restutopopn  23542  ballotlem2  23995  relexpindlem  24440  cnvco1  24675  cnvco2  24676  elfuns  25012  dfiota3  25020  funpartlem  25039  nabi1i  25389  nabi2i  25390  itgaddnclem2  25499  trer  25551  inixp  25723  an43  26035  rmxypairf1o  26319  dsmmacl  26530  pmtrfrn  26723  acsfn1p  26830  pm10.252  26879  pm10.253  26880  pm10.42  26882  2nexaln  26896  aaanv  26910  pm13.195  26936  pm13.196a  26937  rfcnnnub  27030  aovov0bi  27384  jaoi2  27396  nnel  27401  raldifb  27405  tppreqb  27408  f1oun2prg  27424  hashtpg  27471  s4f1o  27504  usgrafilem1  27579  nbgranself2  27602  cusgrasizeindslem1  27636  trls  27688  frgraun  27829  frgra3v  27835  4cycl2vnunb  27850  vdn0frgrav2  27857  vdgn0frgrav2  27858  sbc3org  28040  en3lpVD  28383  3orbi123VD  28388  sbc3orgVD  28389  undif3VD  28420  a9e2ndeqVD  28447  a9e2ndeqALT  28470  bnj115  28513  bnj156  28518  bnj206  28521  bnj110  28652  bnj121  28664  bnj124  28665  bnj130  28668  bnj153  28674  bnj207  28675  bnj605  28701  bnj581  28702  bnj611  28712  bnj864  28716  bnj865  28717  bnj893  28722  bnj1000  28735  bnj978  28743  bnj1040  28764  bnj1049  28766  bnj1133  28781  bnj1189  28801  cleljustNEW7  29045  cleljustALTNEW7  29046  dvelimfOLD7  29128  sb10fOLD7  29169  isopos  29439  islvol5  29837  elpadd0  30067  dvhopellsm  31376  diblsmopel  31430  mapdvalc  31888
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