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

Theorem bicomd 194
Description: Commute two sides of a biconditional in a deduction. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
bicomd.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
bicomd  |-  ( ph  ->  ( ch  <->  ps )
)

Proof of Theorem bicomd
StepHypRef Expression
1 bicomd.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
2 bicom 193 . 2  |-  ( ( ps  <->  ch )  <->  ( ch  <->  ps ) )
31, 2sylib 190 1  |-  ( ph  ->  ( ch  <->  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178
This theorem is referenced by:  impbid2  197  syl5ibr  214  ibir  235  bitr2d  247  bitr3d  248  bitr4d  249  syl5rbb  251  syl6rbb  255  con1bid  322  pm5.5  328  anabs5  786  pm5.55  869  pm5.54  872  baibr  874  baibd  877  rbaibd  878  pm5.75  905  ninba  929  3impexpbicomi  1360  cad1  1390  sbequ12r  1865  sbco  2024  sbco2  2027  cbvab  2404  necon3bbid  2483  necon4bbid  2514  ralcom2  2707  gencbvex  2833  sbhypf  2836  clel3g  2908  reu8  2964  sbceq2a  3005  sbcco2  3017  r19.9rzv  3551  sbcsng  3693  disjxun  4024  opabid  4272  soeq2  4335  ordintdif  4442  tfisi  4650  tfinds2  4655  posn  4759  xpiindi  4822  fvopab6  5584  fconstfv  5697  cbvfo  5762  f1eqcocnv  5768  isoid  5789  isoini  5798  isosolem  5807  f1oweALT  5814  resoprab2  5904  dfoprab3  6139  opiota  6285  tfrlem5  6393  oalimcl  6555  omword  6565  oeword  6585  nnacan  6623  nnmcan  6629  findcard2s  7096  brwdomn0  7280  ssrankr1  7504  r1pw  7514  aleph11  7708  alephval3  7734  gch-kn  8300  wunex2  8357  lttri2  8901  wloglei  9302  divne0b  9432  lemul1  9605  nn0ind-raph  10109  zindd  10110  rebtwnz  10312  qreccl  10333  xrlttri2  10473  xmulneg1  10585  iooshf  10724  difreicc  10763  om2uzlti  11009  expcan  11150  hashbclem  11386  hashf1lem2  11390  absz  11792  iserex  12126  absdvdsb  12543  dvdsabsb  12544  dvdsadd  12563  sadadd2lem2  12637  smupvallem  12670  gcdass  12720  1nprm  12759  lubid  14112  latlem12  14180  odudlatb  14295  issubm2  14422  nsgacs  14649  cycsubg2  14650  gapm  14756  sscntz  14798  odval2  14862  lsmcntz  14984  dfprm2  16443  isopn2  16765  cmpsub  17123  connsub  17143  itg1mulc  19055  lhop1  19357  mdegleb  19446  lawcos  20110  leibpi  20234  ubthlem1  21443  norm-i  21702  hoeq  22334  nmopgt0  22486  pjimai  22750  chirredi  22968  addltmulALT  23020  zmodid2  23416  relexpindlem  23442  colinearalg  23947  eqintg  24361  splint  24448  cnvref  24465  domtri3  24505  domintrefc  24526  mnlmxl2  24670  nelioo5  24912  intopcoaconb  24941  cmptdst  24969  lvsovso2  25028  supnuf  25030  supexr  25032  isfuna  25235  idcatfun  25342  clscnc  25411  pdiveql  25569  topfne  25691  raleqfnOLD  25758  fdc  25856  isidlc  26041  bicomddOLD  26107  istopclsd  26176  eqrabdioph  26258  rexzrexnn0  26286  zindbi  26432  expdiophlem2  26516  islinds3  26705  f1omvdcnv  26788  pm14.122a  27023  stoweidlem13  27163  2reu4a  27348  ralbinrald  27358  afvco2  27418  onfrALTlem5  27580  bitr3VD  27895  onfrALTlem5VD  27931  csbrngVD  27942  islshpsm  28439  lshpkrlem1  28569  opcon1b  28657  lautlt  29549  lauteq  29553  idlaut  29554  diblsmopel  30630  doch11  30832
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