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  1470  nottru  1473  falbitru  1476  nic-dfim  1548  nic-dfneg  1549  2nalexn  1696  2nexaln  1698  sbequ8  1794  dvelimf  2132  cleljust  2163  cleljustALT  2164  sb5rf  2217  sb6rf  2218  sb10f  2252  abeq1i  2558  nne  2631  necon3bbii  2692  necon2abii  2697  necon2bbii  2698  nabbiOLD  2766  nnel  2777  nnelOLD  2778  alexeq  3207  ceqsrexbv  3212  clel2  3214  clel4  3217  2reu5lem1  3283  2reu5lem2  3284  2reu5lem3  3285  dfsbcq2  3308  cbvreucsf  3435  nss  3528  raldifb  3611  difab  3748  un0  3793  in0  3794  ss0b  3798  ssunsn2  4162  rabasiun  4306  iindif2  4371  nssss  4678  opthneg  4701  epse  4837  restidsing  5181  cotrg  5231  issref  5233  mptpreima  5348  ralrnmpt  6046  fmptsng  6100  fmptsnd  6101  dff14a  6185  f13dfv  6188  weniso  6260  uniuni  6614  suppvalbr  6929  eroveu  7466  isfinite2  7835  marypha1lem  7953  marypha2lem4  7958  infcllem  8009  wemapso2lem  8067  en3lplem2  8120  cantnfp1  8185  carden2  8420  fseqenlem1  8453  iscard3  8522  cardnum  8523  alephinit  8524  cardinfima  8526  alephiso  8527  dfac10b  8567  dfackm  8594  isfin5-2  8819  brdom7disj  8957  brdom6disj  8958  fsuppmapnn0fiubex  12201  hashtpg  12632  wrd2ind  12819  splfv1  12847  cshwsexa  12908  s4f1o  12982  cotr2g  13019  relexpindlem  13105  lcmfunsnlem2  14584  ncoprmlnprm  14648  vdwapun  14887  cshwsiun  15033  cshwshash  15038  grpss  16638  pmtrfrn  17050  pmtrrn2  17052  pmtrprfvalrn  17080  issrg  17676  drngnidl  18388  drnglpir  18412  0ringnnzr  18428  unocv  19174  dsmmacl  19235  pmatcollpw2lem  19732  fvmptnn04if  19804  toptopon  19879  ordtbas2  20138  ordtrest2  20151  xmeterval  21378  ovolfcl  22298  eldv  22730  eltayl  23180  musumsum  23984  usgrafilem1  24984  trls  25111  is2wlk  25140  wwlknndef  25310  wlknwwlknvbij  25313  clwwlknndef  25346  clwwlkvbij  25374  el2wlkonotot0  25445  usg2spthonot0  25462  frgraun  25569  frgra2v  25572  4cycl2vnunb  25590  vdn0frgrav2  25596  vdgn0frgrav2  25597  2spotdisj  25634  usg2spot2nb  25638  usgreg2spot  25640  frgraregord013  25691  lejdii  27026  mdslle1i  27805  mdslle2i  27806  mdslj1i  27807  mdslj2i  27808  mo5f  27955  unipreima  28085  2ndpreima  28128  xrge0infss  28181  ordtrest2NEW  28568  ordtconlem1  28569  ballotlem2  29147  plymulx0  29224  bnj115  29319  bnj156  29324  bnj206  29327  bnj110  29457  bnj121  29469  bnj124  29470  bnj130  29473  bnj153  29479  bnj207  29480  bnj581  29507  bnj611  29517  bnj864  29521  bnj865  29522  bnj893  29527  bnj1000  29540  bnj978  29548  bnj1040  29569  bnj1049  29571  bnj1133  29586  bnj1189  29606  cnvco1  30187  cnvco2  30188  dfiota3  30475  trer  30757  nabi1i  30837  nabi2i  30838  bj-dfifc2  30943  bj-df-ifc  30944  bj-nf3  30976  bj-hbext  31044  bj-cleljust  31124  bj-denotes  31218  bj-ralcom4  31228  bj-rexcom4  31229  bj-elsngl  31311  bj-nuliotaALT  31372  topdifinfeq  31487  isbasisrelowllem2  31493  wl-sb8eut  31609  inixp  31758  notbinot1  32015  notbinot2  32019  truconj  32040  sbccom2lem  32067  sbccom2  32068  sbccom2f  32069  tsim1  32075  tsxo3  32084  tsxo4  32085  an43  32127  isopos  32454  islvol5  32852  elpadd0  33082  dvhopellsm  34393  diblsmopel  34447  mapdvalc  34905  rmxypairf1o  35464  acsfn1p  35763  ifpnotnotb  35821  ifpdfxor  35829  ifpidg  35833  ifpim123g  35842  ifpim1g  35843  ifpimimb  35846  ifpimim  35851  rp-fakeanorass  35855  rp-isfinite6  35861  cnviun  35880  dfxor4  35996  dfhe3  36006  dffrege69  36164  dffrege76  36171  pm10.252  36346  pm10.253  36347  pm10.42  36349  aaanv  36374  pm13.195  36400  pm13.196a  36401  sbc3or  36525  sbc3orgOLD  36529  en3lpVD  36880  3orbi123VD  36885  sbc3orgVD  36886  undif3VD  36918  ax6e2ndeqVD  36945  ax6e2ndeqALT  36967  sineq0ALT  36973  uzwo4  37032  rnmptpr  37065  fompt  37089  cncfshift  37322  dvnmul  37386  dvnprodlem2  37390  sge00  37751  sge0iunmpt  37793  meadjiun  37812  carageneld  37831  aibandbiaiffaiffb  37880  plcofph  37924  pldofph  37925  plvcofph  37926  aovov0bi  38087  icceuelpartlem  38138  rexdifpr  38376  usgfislem1  38513  usgfisALTlem1  38517  copisnmnd  38566  pgrpgt2nabl  38910  lindslinindsimp2lem5  39014  islininds2  39036  ldepslinc  39061
  Copyright terms: Public domain W3C validator