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

Theorem bicomi 205
Description: Inference from commutative law for logical equivalence. (Contributed by NM, 3-Jan-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 202 . 2  |-  ( (
ph 
<->  ps )  ->  ( ps 
<-> 
ph ) )
31, 2ax-mp 5 1  |-  ( ps  <->  ph )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 188
This theorem is referenced by:  biimpri  209  bitr2i  253  bitr3i  254  bitr4i  255  syl5bbr  262  syl5rbbr  263  syl6bbr  266  syl6rbbr  267  mtbir  300  sylnibr  306  sylnbir  308  xchnxbir  310  xchbinxr  312  con1bii  332  con2bii  333  nbn  348  xor3  358  pm5.41  365  pm4.64  373  pm4.63  422  pm4.61  427  anor  491  pm4.53  494  pm4.55  496  pm4.56  497  pm4.57  499  pm4.25  517  pm4.87  586  anidm  648  pm4.77  794  anabs1  815  anabs7  817  pm4.76  874  pm5.63  932  3ianor  999  3oran  1001  pm3.2an3  1184  syl3anbr  1308  3an6  1345  nannot  1387  nanbi  1388  nanbiOLD  1389  truan  1454  truimfal  1468  nottru  1471  falbitru  1474  nic-dfim  1546  nic-dfneg  1547  2nalexn  1694  2nexaln  1696  sbequ8  1795  dvelimf  2135  cleljust  2166  cleljustALT  2167  sb5rf  2220  sb6rf  2221  sb10f  2255  abeq1i  2546  nne  2620  necon3bbii  2681  necon2abii  2686  necon2bbii  2687  nabbiOLD  2755  nnel  2766  nnelOLD  2767  ceqsrexbv  3205  clel2  3207  clel4  3210  2reu5lem1  3277  2reu5lem2  3278  2reu5lem3  3279  dfsbcq2  3302  cbvreucsf  3429  nss  3522  raldifb  3605  difab  3742  un0  3789  in0  3790  ss0b  3794  ssunsn2  4159  rabasiun  4303  iindif2  4368  nssss  4677  opthneg  4700  epse  4836  restidsing  5180  cotrg  5230  issref  5232  mptpreima  5347  ralrnmpt  6046  fmptsng  6100  fmptsnd  6101  dff14a  6185  f13dfv  6188  weniso  6260  uniuni  6614  suppvalbr  6929  eroveu  7469  isfinite2  7838  marypha1lem  7956  marypha2lem4  7961  infcllem  8012  wemapso2lem  8076  en3lplem2  8129  cantnfp1  8194  carden2  8429  fseqenlem1  8462  iscard3  8531  cardnum  8532  alephinit  8533  cardinfima  8535  alephiso  8536  dfac10b  8576  dfackm  8603  isfin5-2  8828  brdom7disj  8966  brdom6disj  8967  fsuppmapnn0fiubex  12210  hash2prb  12637  hashtpg  12645  wrd2ind  12836  splfv1  12864  cshwsexa  12925  s4f1o  13003  cotr2g  13040  relexpindlem  13126  lcmfunsnlem2  14612  ncoprmlnprm  14676  vdwapun  14923  cshwsiun  15069  cshwshash  15074  grpss  16686  pmtrfrn  17098  pmtrrn2  17100  pmtrprfvalrn  17128  issrg  17740  drngnidl  18452  drnglpir  18476  0ringnnzr  18492  unocv  19241  dsmmacl  19302  pmatcollpw2lem  19799  fvmptnn04if  19871  toptopon  19946  ordtbas2  20205  ordtrest2  20218  xmeterval  21445  ovolfcl  22417  eldv  22851  eltayl  23313  musumsum  24119  usgrafilem1  25137  trls  25264  is2wlk  25293  wwlknndef  25463  wlknwwlknvbij  25466  clwwlknndef  25499  clwwlkvbij  25527  el2wlkonotot0  25598  usg2spthonot0  25615  frgraun  25722  frgra2v  25725  4cycl2vnunb  25743  vdn0frgrav2  25749  vdgn0frgrav2  25750  2spotdisj  25787  usg2spot2nb  25791  usgreg2spot  25793  frgraregord013  25844  lejdii  27189  mdslle1i  27968  mdslle2i  27969  mdslj1i  27970  mdslj2i  27971  mo5f  28118  unipreima  28247  2ndpreima  28290  xrge0infssOLD  28347  ordtrest2NEW  28737  ordtconlem1  28738  ballotlem2  29329  plymulx0  29444  bnj115  29539  bnj156  29544  bnj206  29547  bnj110  29677  bnj121  29689  bnj124  29690  bnj130  29693  bnj153  29699  bnj207  29700  bnj581  29727  bnj611  29737  bnj864  29741  bnj865  29742  bnj893  29747  bnj1000  29760  bnj978  29768  bnj1040  29789  bnj1049  29791  bnj1133  29806  bnj1189  29826  cnvco1  30407  cnvco2  30408  dfiota3  30695  trer  30977  nabi1i  31057  nabi2i  31058  bj-dfifc2  31163  bj-df-ifc  31164  bj-nf3  31196  bj-hbext  31264  bj-cleljust  31343  bj-denotes  31437  bj-ralcom4  31447  bj-rexcom4  31448  bj-elsngl  31530  bj-nuliotaALT  31591  con1bii2  31698  con2bii2  31699  topdifinfeq  31717  isbasisrelowllem2  31723  wl-sb8eut  31870  inixp  32019  notbinot1  32276  notbinot2  32280  truconj  32301  sbccom2lem  32328  sbccom2  32329  sbccom2f  32330  tsim1  32336  tsxo3  32345  tsxo4  32346  an43  32388  isopos  32715  islvol5  33113  elpadd0  33343  dvhopellsm  34654  diblsmopel  34708  mapdvalc  35166  rmxypairf1o  35729  acsfn1p  36035  ifpnotnotb  36093  ifpdfxor  36101  ifpidg  36105  ifpim123g  36114  ifpim1g  36115  ifpimimb  36118  ifpimim  36123  rp-fakeanorass  36127  rp-isfinite6  36133  elmapintrab  36152  undmrnresiss  36180  clcnvlem  36200  cnviun  36212  dfxor4  36328  dfhe3  36340  dffrege69  36498  dffrege76  36505  pm10.252  36680  pm10.253  36681  pm10.42  36683  aaanv  36708  pm13.195  36734  pm13.196a  36735  sbc3or  36859  sbc3orgOLD  36863  en3lpVD  37214  3orbi123VD  37219  sbc3orgVD  37220  undif3VD  37252  ax6e2ndeqVD  37279  ax6e2ndeqALT  37301  sineq0ALT  37307  uzwo4  37365  rnmptpr  37404  fompt  37428  cncfshift  37691  dvnmul  37758  dvnprodlem2  37762  sge00  38126  sge0iunmpt  38168  meadjiun  38212  carageneld  38231  ovncvrrp  38290  aibandbiaiffaiffb  38352  plcofph  38403  pldofph  38404  plvcofph  38405  plvcofphax  38406  plvofpos  38407  aovov0bi  38568  icceuelpartlem  38619  rexdifpr  38860  ausgrusgrb  39047  cplgr3v  39259  usgfislem1  39376  usgfisALTlem1  39380  copisnmnd  39429  pgrpgt2nabl  39773  lindslinindsimp2lem5  39877  islininds2  39899  ldepslinc  39924
  Copyright terms: Public domain W3C validator