MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bicomd Structured version   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 4    <-> 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  1378  cad1  1408  sbequ12r  1948  sbco  2164  sbco2  2167  cbvab  2560  necon3bbid  2641  necon4bbid  2675  ralcom2  2878  gencbvex  3004  sbhypf  3007  clel3g  3079  reu8  3136  sbceq2a  3178  sbcco2  3190  r19.9rzv  3746  sbcsng  3889  disjxun  4235  opabid  4490  soeq2  4552  ordintdif  4659  tfisi  4867  tfinds2  4872  posn  4975  xpiindi  5039  fvopab6  5855  fconstfv  5983  cbvfo  6051  f1eqcocnv  6057  isoid  6078  isoini  6087  isosolem  6096  f1oweALT  6103  resoprab2  6196  dfoprab3  6432  opiota  6564  tfrlem5  6670  oalimcl  6832  omword  6842  oeword  6862  nnacan  6900  nnmcan  6906  findcard2s  7378  brwdomn0  7566  ssrankr1  7790  r1pw  7800  aleph11  7996  alephval3  8022  gch-kn  8583  wunex2  8644  lttri2  9188  wloglei  9590  divne0b  9720  lemul1  9893  nn0ind-raph  10401  zindd  10402  rebtwnz  10604  qreccl  10625  xrlttri2  10766  xmulneg1  10879  iooshf  11020  difreicc  11059  elfznelfzo  11223  om2uzlti  11321  expcan  11463  hashvnfin  11673  hashgt0elex  11701  hashgt12el  11713  hashgt12el2  11714  hashbclem  11732  hashf1lem2  11736  absz  12147  iserex  12481  absdvdsb  12899  dvdsabsb  12900  dvdsadd  12919  sadadd2lem2  12993  smupvallem  13026  gcdass  13076  1nprm  13115  lubid  14470  latlem12  14538  odudlatb  14653  issubm2  14780  nsgacs  15007  cycsubg2  15008  gapm  15114  sscntz  15156  odval2  15220  lsmcntz  15342  dfprm2  16805  isopn2  17127  cmpsub  17494  connsub  17515  itg1mulc  19625  lhop1  19929  mdegleb  20018  lawcos  20689  leibpi  20813  ausisusgra  21411  usgraedg4  21437  usgraidx2v  21443  nbgraf1olem1  21482  nb3graprlem1  21491  nb3grapr  21493  nb3grapr2  21494  cusgrarn  21499  uvtx01vtx  21532  redwlk  21637  wlkdvspthlem  21638  wlkdvspth  21639  ubthlem1  22403  norm-i  22662  hoeq  23294  nmopgt0  23446  pjimai  23710  chirredi  23928  addltmulALT  23980  iunrdx  24045  disjrdx  24062  zmodid2  25145  relexpindlem  25170  prodrb  25289  nofulllem2  25689  colinearalg  25880  sin2h  26274  mbfresfi  26289  itg2addnclem  26294  itg2addnclem2  26295  itg2addnclem3  26296  ftc1anclem1  26318  topfne  26408  isidlc  26663  istopclsd  26792  eqrabdioph  26874  rexzrexnn0  26902  zindbi  27047  expdiophlem2  27131  islinds3  27319  f1omvdcnv  27402  pm14.122a  27637  2reu4a  27981  ralbinrald  27991  afvco2  28054  elfzomelpfzo  28176  subsubelfzo0  28182  fzofzim  28183  2submod  28199  swrd0swrd  28255  swrdswrd  28257  swrdccat3  28273  cshwidxmod  28301  2cshw2lem2  28311  2cshwmod  28315  2wlkeq  28365  wlkiswwlk1  28396  el2spthonot0  28427  el2wlkonotot  28429  el2wlkonotot1  28430  el2wlksotot  28438  usg2wlkonot  28439  2pthwlkonot  28441  usg2spthonot  28444  usg2spthonot0  28445  frgrancvvdeqlemC  28526  frgraeu  28541  frg2woteq  28547  onfrALTlem5  28726  bitr3VD  29059  onfrALTlem5VD  29095  csbrngVD  29106  nfsb4twAUX7  29674  sbcoNEW7  29680  sbco2wAUX7  29683  sbco2OLD7  29850  islshpsm  29876  lshpkrlem1  30006  opcon1b  30094  lautlt  30986  lauteq  30990  idlaut  30991  diblsmopel  32067  doch11  32269
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 179
  Copyright terms: Public domain W3C validator