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, 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 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  299  sylnibr  305  sylnbir  307  xchnxbir  309  xchbinxr  311  con1bii  331  con2bii  332  nbn  347  xor3  357  pm5.41  364  pm4.64  372  pm4.63  421  pm4.61  426  anor  486  pm4.53  489  pm4.55  491  pm4.56  492  pm4.57  494  pm4.25  512  pm4.87  579  anidm  637  pm4.77  778  anabs1  799  anabs7  801  pm4.76  854  pm5.63  908  jaoi2OLD  953  3ianor  975  3oran  977  pm3.2an3  1160  syl3anbr  1255  3an6  1292  nannot  1332  truan  1379  truimfal  1395  nottru  1398  nic-dfim  1479  nic-dfneg  1480  2nalexn  1622  2nexaln  1624  sbequ8  1704  dvelimf  2025  cleljust  2056  cleljustALT  2057  sb5rf  2122  sb6rf  2124  sb10f  2168  nne  2602  necon3bbii  2629  necon2abii  2656  necon2bbii  2657  nabbi  2696  nnel  2704  alexeq  3078  ceqsrexbv  3083  clel2  3085  clel4  3088  2reu5lem1  3153  2reu5lem2  3154  2reu5lem3  3155  dfsbcq2  3178  cbvreucsf  3309  nss  3402  raldifb  3484  difab  3607  un0  3650  in0  3651  ss0b  3655  ssunsn2  4020  iindif2  4227  nssss  4536  opthneg  4559  epse  4690  restidsing  5150  cotr  5198  issref  5199  mptpreima  5319  ralrnmpt  5840  fmptsng  5887  weniso  6032  uniuni  6374  suppvalbr  6683  eroveu  7183  isfinite2  7558  marypha1lem  7671  marypha2lem4  7676  wemapso2lem  7755  en3lplem2  7809  cantnfp1  7877  carden2  8145  fseqenlem1  8182  iscard3  8251  cardnum  8252  alephinit  8253  cardinfima  8255  alephiso  8256  dfac10b  8296  dfackm  8323  isfin5-2  8548  brdom7disj  8686  brdom6disj  8687  hashtpg  12170  wrdeqswrdlsw  12327  wrd2ind  12356  splfv1  12381  cshwsexa  12442  s4f1o  12512  vdwapun  14018  cshwsiun  14109  cshwshash  14114  grpss  15539  pmtrfrn  15944  pmtrrn2  15946  pmtrprfvalrn  15974  drngnidl  17233  drnglpir  17257  unocv  17947  dsmmacl  18008  toptopon  18380  ordtbas2  18637  ordtrest2  18650  restutopopn  19655  xmeterval  19849  ovolfcl  20792  eldv  21215  eltayl  21710  musumsum  22417  usgrafilem1  23147  trls  23258  is2wlk  23287  lejdii  24764  mdslle1i  25544  mdslle2i  25545  mdslj1i  25546  mdslj2i  25547  spc2ed  25680  mo5f  25692  unipreima  25785  2ndpreima  25826  issrg  26042  ordtrest2NEW  26207  ordtconlem1  26208  ballotlem2  26719  plymulx0  26796  relexpindlem  27188  fprod2dlem  27338  cnvco1  27417  cnvco2  27418  dfiota3  27801  nabi1i  28085  nabi2i  28086  wl-sb8eut  28242  trer  28355  inixp  28466  notbinot1  28723  impor  28725  notbinot2  28727  truconj  28748  sbcalf  28764  sbcexf  28765  exlimddvfi  28774  sbccom2lem  28777  sbccom2  28778  sbccom2f  28779  tsim1  28785  tsxo3  28794  tsxo4  28795  sbcom3OLD  28824  an43  28838  rmxypairf1o  29097  acsfn1p  29401  pm10.252  29458  pm10.253  29459  pm10.42  29461  aaanv  29486  pm13.195  29512  pm13.196a  29513  aibandbiaiffaiffb  29754  aovov0bi  29948  rexdifpr  29970  dff14a  29990  f13dfv  29993  rabasiun  30076  wwlknndef  30215  wlknwwlknvbij  30218  el2wlkonotot0  30237  usg2spthonot0  30254  clwwlknndef  30282  clwwlkvbij  30309  frgraun  30434  frgra2v  30437  4cycl2vnunb  30455  vdn0frgrav2  30462  vdgn0frgrav2  30463  2spotdisj  30500  usg2spot2nb  30504  usgreg2spot  30506  frgraregord013  30557  fmptsnd  30567  pgrpgt2nabel  30600  0rngnnzr  30609  lindslinindsimp2lem5  30705  islininds2  30727  ldepslinc  30760  sbc3or  30938  sbc3orgOLD  30939  en3lpVD  31283  3orbi123VD  31288  sbc3orgVD  31289  undif3VD  31320  ax6e2ndeqVD  31347  ax6e2ndeqALT  31369  sineq0ALT  31375  bnj115  31416  bnj156  31421  bnj206  31424  bnj110  31553  bnj121  31565  bnj124  31566  bnj130  31569  bnj153  31575  bnj207  31576  bnj581  31603  bnj611  31613  bnj864  31617  bnj865  31618  bnj893  31623  bnj1000  31636  bnj978  31644  bnj1040  31665  bnj1049  31667  bnj1133  31682  bnj1189  31702  bj-nf3  31796  bj-nfdt  31833  bj-cleljust  31906  bj-denotes  31977  bj-issetw  31978  bj-ralcom4  31984  bj-rexcom4  31985  bj-elsngl  32044  isopos  32398  islvol5  32796  elpadd0  33026  dvhopellsm  34335  diblsmopel  34389  mapdvalc  34847
  Copyright terms: Public domain W3C validator