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

Theorem bicomd 193
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 192 . 2  |-  ( ( ps  <->  ch )  <->  ( ch  <->  ps ) )
31, 2sylib 189 1  |-  ( ph  ->  ( ch  <->  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  impbid2  196  syl5ibr  213  ibir  234  bitr2d  246  bitr3d  247  bitr4d  248  syl5rbb  250  syl6rbb  254  con1bid  321  pm5.5  327  anabs5  785  pm5.55  868  pm5.54  871  baibr  873  baibd  876  rbaibd  877  pm5.75  904  ninba  928  3impexpbicomi  1374  cad1  1404  sbequ12r  1934  dvelimv  1977  sbco  2117  sbco2  2120  cbvab  2506  necon3bbid  2585  necon4bbid  2616  ralcom2  2816  gencbvex  2942  sbhypf  2945  clel3g  3017  reu8  3074  sbceq2a  3116  sbcco2  3128  r19.9rzv  3666  sbcsng  3809  disjxun  4152  opabid  4403  soeq2  4465  ordintdif  4572  tfisi  4779  tfinds2  4784  posn  4887  xpiindi  4951  fvopab6  5766  fconstfv  5894  cbvfo  5962  f1eqcocnv  5968  isoid  5989  isoini  5998  isosolem  6007  f1oweALT  6014  resoprab2  6107  dfoprab3  6343  opiota  6472  tfrlem5  6578  oalimcl  6740  omword  6750  oeword  6770  nnacan  6808  nnmcan  6814  findcard2s  7286  brwdomn0  7471  ssrankr1  7695  r1pw  7705  aleph11  7899  alephval3  7925  gch-kn  8490  wunex2  8547  lttri2  9091  wloglei  9492  divne0b  9622  lemul1  9795  nn0ind-raph  10303  zindd  10304  rebtwnz  10506  qreccl  10527  xrlttri2  10668  xmulneg1  10781  iooshf  10922  difreicc  10961  elfznelfzo  11120  om2uzlti  11218  expcan  11360  hashvnfin  11570  hashgt0elex  11598  hashgt12el  11610  hashgt12el2  11611  hashbclem  11629  hashf1lem2  11633  absz  12044  iserex  12378  absdvdsb  12796  dvdsabsb  12797  dvdsadd  12816  sadadd2lem2  12890  smupvallem  12923  gcdass  12973  1nprm  13012  lubid  14367  latlem12  14435  odudlatb  14550  issubm2  14677  nsgacs  14904  cycsubg2  14905  gapm  15011  sscntz  15053  odval2  15117  lsmcntz  15239  dfprm2  16698  isopn2  17020  cmpsub  17386  connsub  17406  itg1mulc  19464  lhop1  19766  mdegleb  19855  lawcos  20526  leibpi  20650  ausisusgra  21248  usgraedg4  21273  usgraidx2v  21279  nbgraf1olem1  21318  nb3graprlem1  21327  nb3grapr  21329  nb3grapr2  21330  cusgrarn  21335  uvtx01vtx  21368  redwlk  21455  wlkdvspthlem  21456  wlkdvspth  21457  ubthlem1  22221  norm-i  22480  hoeq  23112  nmopgt0  23264  pjimai  23528  chirredi  23746  addltmulALT  23798  iunrdx  23859  disjrdx  23875  zmodid2  24894  relexpindlem  24919  prodrb  25038  nofulllem2  25382  colinearalg  25564  itg2addnclem  25958  itg2addnclem2  25959  itg2addnc  25960  topfne  26062  isidlc  26317  istopclsd  26446  eqrabdioph  26528  rexzrexnn0  26556  zindbi  26701  expdiophlem2  26785  islinds3  26974  f1omvdcnv  27057  pm14.122a  27292  2reu4a  27636  ralbinrald  27646  afvco2  27710  frgrancvvdeqlemC  27792  onfrALTlem5  27972  bitr3VD  28303  onfrALTlem5VD  28339  csbrngVD  28350  nfsb4twAUX7  28913  sbcoNEW7  28918  sbco2wAUX7  28921  sbco2OLD7  29069  islshpsm  29096  lshpkrlem1  29226  opcon1b  29314  lautlt  30206  lauteq  30210  idlaut  30211  diblsmopel  31287  doch11  31489
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator