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  570  anidm  628  pm4.77  765  anabs1  786  anabs7  788  pm4.76  841  pm5.63  895  3ianor  954  3oran  956  pm3.2an3  1136  syl3anbr  1231  3an6  1267  nannot  1298  truimfal  1341  nottru  1344  nic-dfim  1429  nic-dfneg  1430  2nalexn  1571  sbid  1896  dvelimf  1976  cleljust  2063  sb10f  2085  nne  2425  necon3bbii  2452  necon2abii  2476  necon2bbii  2477  alexeq  2872  ceqsrexbv  2877  clel2  2879  clel4  2882  2reu5lem1  2945  2reu5lem2  2946  2reu5lem3  2947  dfsbcq2  2969  cbvreucsf  3120  nss  3211  difab  3412  un0  3454  in0  3455  ss0b  3459  ssunsn2  3747  iindif2  3945  nssss  4201  epse  4348  uniuni  4499  reusv2lem4  4510  cotr  5043  issref  5044  mptpreima  5153  ralrnmpt  5603  weniso  5786  eroveu  6721  isfinite2  7083  marypha1lem  7154  marypha2lem4  7159  en3lplem2  7385  carden2  7588  fseqenlem1  7619  iscard3  7688  cardnum  7689  alephinit  7690  cardinfima  7692  alephiso  7693  dfac10b  7733  dfackm  7760  isfin5-2  7985  brdom7disj  8124  brdom6disj  8125  splfv1  11435  vdwapun  12983  grpss  14465  drngnidl  15943  drnglpir  15967  unocv  16542  toptopon  16633  ordtbas2  16883  ordtrest2  16896  xmeterval  17940  ovolfcl  18788  eldv  19210  eltayl  19701  musumsum  20394  lejdii  22077  mdslle1i  22857  mdslle2i  22858  mdslj1i  22859  mdslj2i  22860  ballotlem2  23008  relexpindlem  23408  cnvco1  23488  cnvco2  23489  dfiota3  23837  funpartfv  23858  nabi1i  24205  nabi2i  24206  negcmpprcal2  24312  eqvinopb  24331  boxeq  24353  notev  24356  notal  24357  albineal  24365  splint  24414  restidsing  24442  imfstnrelc  24447  defse3  24639  qusp  24909  algi  25094  prismorcsetlemc  25284  nbssntrs  25514  trer  25594  inixp  25766  an43  26079  rmxypairf1o  26363  dsmmacl  26574  pmtrfrn  26767  acsfn1p  26874  pm10.252  26923  pm10.253  26924  pm10.42  26926  2nexaln  26940  aaanv  26954  pm13.195  26981  pm13.196a  26982  rfcnnnub  27075  sbc3org  27348  en3lpVD  27671  3orbi123VD  27676  sbc3orgVD  27677  undif3VD  27708  a9e2ndeqVD  27735  a9e2ndeqALT  27758  bnj115  27800  bnj156  27805  bnj206  27808  bnj110  27939  bnj121  27951  bnj124  27952  bnj130  27955  bnj153  27961  bnj207  27962  bnj605  27988  bnj581  27989  bnj611  27999  bnj864  28003  bnj865  28004  bnj893  28009  bnj1000  28022  bnj978  28030  bnj1040  28051  bnj1049  28053  bnj1133  28068  bnj1189  28088  19.8vK  28171  isopos  28537  islvol5  28935  elpadd0  29165  dvhopellsm  30474  diblsmopel  30528  mapdvalc  30986
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