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  787  pm5.55  872  pm5.54  875  baibr  877  baibd  880  rbaibd  881  pm5.75  908  ninba  932  3impexpbicomi  1364  cad1  1394  sbequ12r  1894  sbco  1978  sbco2  1981  cbvab  2374  necon3bbid  2453  necon4bbid  2484  ralcom2  2677  gencbvex  2798  sbhypf  2801  clel3g  2873  reu8  2929  sbceq2a  2963  sbcco2  2975  r19.9rzv  3509  sbcsng  3650  disjxun  3981  opabid  4229  soeq2  4292  ordintdif  4399  tfisi  4607  tfinds2  4612  posn  4732  xpiindi  4795  fvopab6  5541  fconstfv  5654  cbvfo  5719  f1eqcocnv  5725  isoid  5746  isoini  5755  isosolem  5764  f1oweALT  5771  resoprab2  5861  dfoprab3  6096  opiota  6242  tfrlem5  6350  oalimcl  6512  omword  6522  oeword  6542  nnacan  6580  nnmcan  6586  findcard2s  7053  brwdomn0  7237  ssrankr1  7461  r1pw  7471  aleph11  7665  alephval3  7691  gch-kn  8257  wunex2  8314  lttri2  8858  wloglei  9259  divne0b  9389  lemul1  9562  nn0ind-raph  10065  zindd  10066  rebtwnz  10268  qreccl  10289  xrlttri2  10429  xmulneg1  10541  iooshf  10680  difreicc  10719  om2uzlti  10965  expcan  11106  hashbclem  11341  hashf1lem2  11345  absz  11747  iserex  12081  absdvdsb  12495  dvdsabsb  12496  dvdsadd  12515  sadadd2lem2  12589  smupvallem  12622  gcdass  12672  1nprm  12711  lubid  14064  latlem12  14132  odudlatb  14247  issubm2  14374  nsgacs  14601  cycsubg2  14602  gapm  14708  sscntz  14750  odval2  14814  lsmcntz  14936  dfprime2  16395  isopn2  16717  cmpsub  17075  connsub  17095  itg1mulc  19007  lhop1  19309  mdegleb  19398  lawcos  20062  leibpi  20186  ubthlem1  21395  norm-i  21654  hoeq  22286  nmopgt0  22438  pjimai  22702  chirredi  22920  addltmulALT  22972  zmodid2  23368  relexpindlem  23394  colinearalg  23899  eqintg  24313  splint  24400  cnvref  24417  domtri3  24457  domintrefc  24478  mnlmxl2  24622  nelioo5  24864  intopcoaconb  24893  cmptdst  24921  lvsovso2  24980  supnuf  24982  supexr  24984  isfuna  25187  idcatfun  25294  clscnc  25363  pdiveql  25521  topfne  25643  raleqfnOLD  25710  fdc  25808  isidlc  25993  bicomddOLD  26059  istopclsd  26128  eqrabdioph  26210  rexzrexnn0  26238  zindbi  26384  expdiophlem2  26468  islinds3  26657  f1omvdcnv  26740  pm14.122a  26976  stoweidlem13  27083  onfrALTlem5  27344  bitr3VD  27659  onfrALTlem5VD  27695  csbrngVD  27706  islshpsm  28321  lshpkrlem1  28451  opcon1b  28539  lautlt  29431  lauteq  29435  idlaut  29436  diblsmopel  30512  doch11  30714
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