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

Theorem bicomi 202
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 199 . 2  |-  ( (
ph 
<->  ps )  ->  ( ps 
<-> 
ph ) )
31, 2ax-mp 5 1  |-  ( ps  <->  ph )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184
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 185
This theorem is referenced by:  biimpri  206  bitr2i  250  bitr3i  251  bitr4i  252  syl5bbr  259  syl5rbbr  260  syl6bbr  263  syl6rbbr  264  mtbir  297  sylnibr  303  sylnbir  305  xchnxbir  307  xchbinxr  309  con1bii  329  con2bii  330  nbn  345  xor3  355  pm5.41  362  pm4.64  370  pm4.63  419  pm4.61  424  anor  487  pm4.53  490  pm4.55  492  pm4.56  493  pm4.57  495  pm4.25  513  pm4.87  582  anidm  642  pm4.77  785  anabs1  806  anabs7  808  pm4.76  864  pm5.63  922  3ianor  988  3oran  990  pm3.2an3  1173  syl3anbr  1270  3an6  1307  nannot  1349  nanbi  1350  nanbiOLD  1351  truan  1416  truimfal  1432  nottru  1435  falbitru  1438  nic-dfim  1509  nic-dfneg  1510  2nalexn  1657  2nexaln  1659  sbequ8  1752  dvelimf  2082  cleljust  2113  cleljustALT  2114  sb5rf  2169  sb6rf  2170  sb10f  2204  abeq1i  2511  nne  2583  necon3bbii  2643  necon2abii  2648  necon2bbii  2649  nabbiOLD  2716  nnel  2727  nnelOLD  2728  alexeq  3154  ceqsrexbv  3159  clel2  3161  clel4  3164  2reu5lem1  3230  2reu5lem2  3231  2reu5lem3  3232  dfsbcq2  3255  cbvreucsf  3382  nss  3475  raldifb  3558  difab  3692  un0  3737  in0  3738  ss0b  3742  ssunsn2  4103  rabasiun  4247  iindif2  4312  nssss  4618  opthneg  4641  epse  4776  restidsing  5242  cotrg  5291  issref  5293  mptpreima  5408  ralrnmpt  5942  fmptsng  5994  fmptsnd  5995  dff14a  6078  f13dfv  6081  weniso  6151  uniuni  6508  suppvalbr  6821  eroveu  7324  isfinite2  7693  marypha1lem  7808  marypha2lem4  7813  wemapso2lem  7893  en3lplem2  7946  cantnfp1  8013  carden2  8281  fseqenlem1  8318  iscard3  8387  cardnum  8388  alephinit  8389  cardinfima  8391  alephiso  8392  dfac10b  8432  dfackm  8459  isfin5-2  8684  brdom7disj  8822  brdom6disj  8823  fsuppmapnn0fiubex  12001  hashtpg  12427  wrd2ind  12614  splfv1  12642  cshwsexa  12703  s4f1o  12777  cotr2g  12814  trclfvcotr  12847  relexpindlem  12898  vdwapun  14494  cshwsiun  14586  cshwshash  14591  grpss  16188  pmtrfrn  16600  pmtrrn2  16602  pmtrprfvalrn  16630  issrg  17272  drngnidl  17990  drnglpir  18014  0ringnnzr  18030  unocv  18802  dsmmacl  18863  pmatcollpw2lem  19363  fvmptnn04if  19435  toptopon  19519  ordtbas2  19778  ordtrest2  19791  xmeterval  21020  ovolfcl  21963  eldv  22387  eltayl  22840  musumsum  23585  usgrafilem1  24532  trls  24659  is2wlk  24688  wwlknndef  24858  wlknwwlknvbij  24861  clwwlknndef  24894  clwwlkvbij  24922  el2wlkonotot0  24993  usg2spthonot0  25010  frgraun  25117  frgra2v  25120  4cycl2vnunb  25138  vdn0frgrav2  25144  vdgn0frgrav2  25145  2spotdisj  25182  usg2spot2nb  25186  usgreg2spot  25188  frgraregord013  25239  lejdii  26573  mdslle1i  27352  mdslle2i  27353  mdslj1i  27354  mdslj2i  27355  mo5f  27500  unipreima  27624  2ndpreima  27673  xrge0infss  27730  ordtrest2NEW  28059  ordtconlem1  28060  ballotlem2  28610  plymulx0  28687  cnvco1  29355  cnvco2  29356  dfiota3  29726  nabi1i  30010  nabi2i  30011  wl-sb8eut  30187  trer  30300  inixp  30385  notbinot1  30642  notbinot2  30646  truconj  30667  sbccom2lem  30695  sbccom2  30696  sbccom2f  30697  tsim1  30703  tsxo3  30712  tsxo4  30713  an43  30755  rmxypairf1o  31012  acsfn1p  31316  pm10.252  31434  pm10.253  31435  pm10.42  31437  aaanv  31462  pm13.195  31488  pm13.196a  31489  cncfshift  31842  dvnmul  31906  dvnprodlem2  31910  aibandbiaiffaiffb  32255  aovov0bi  32447  rexdifpr  32621  usgfislem1  32762  usgfisALTlem1  32766  copisnmnd  32815  pgrpgt2nabl  33159  lindslinindsimp2lem5  33263  islininds2  33285  ldepslinc  33310  sbc3or  33635  sbc3orgOLD  33639  en3lpVD  33991  3orbi123VD  33996  sbc3orgVD  33997  undif3VD  34029  ax6e2ndeqVD  34056  ax6e2ndeqALT  34078  sineq0ALT  34084  bnj115  34125  bnj156  34130  bnj206  34133  bnj110  34263  bnj121  34275  bnj124  34276  bnj130  34279  bnj153  34285  bnj207  34286  bnj581  34313  bnj611  34323  bnj864  34327  bnj865  34328  bnj893  34333  bnj1000  34346  bnj978  34354  bnj1040  34375  bnj1049  34377  bnj1133  34392  bnj1189  34412  bj-dfifc2  34511  bj-df-ifc  34512  bj-nf3  34544  bj-hbext  34611  bj-cleljust  34691  bj-denotes  34781  bj-ralcom4  34791  bj-rexcom4  34792  bj-elsngl  34874  bj-nuliotaALT  34935  isopos  35318  islvol5  35716  elpadd0  35946  dvhopellsm  37257  diblsmopel  37311  mapdvalc  37769  ifpim123g  38119  ifpidg  38121  ifpim1g  38131  ifpimimb  38132  ifpimim  38133  ifpnotnotb  38141  ifpororb  38149  ifpdfxor  38162  rp-fakeanorass  38167  rp-isfinite6  38173  cnviun  38190  dfxor4  38259  dfhe3  38269  dffrege69  38431  dffrege76  38438
  Copyright terms: Public domain W3C validator