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  1941  spei  1964  sbco  2140  sbco2  2143  cbvab  2530  necon3bbid  2609  necon4bbid  2640  ralcom2  2840  gencbvex  2966  sbhypf  2969  clel3g  3041  reu8  3098  sbceq2a  3140  sbcco2  3152  r19.9rzv  3690  sbcsng  3833  disjxun  4178  opabid  4429  soeq2  4491  ordintdif  4598  tfisi  4805  tfinds2  4810  posn  4913  xpiindi  4977  fvopab6  5793  fconstfv  5921  cbvfo  5989  f1eqcocnv  5995  isoid  6016  isoini  6025  isosolem  6034  f1oweALT  6041  resoprab2  6134  dfoprab3  6370  opiota  6502  tfrlem5  6608  oalimcl  6770  omword  6780  oeword  6800  nnacan  6838  nnmcan  6844  findcard2s  7316  brwdomn0  7501  ssrankr1  7725  r1pw  7735  aleph11  7929  alephval3  7955  gch-kn  8520  wunex2  8577  lttri2  9121  wloglei  9523  divne0b  9653  lemul1  9826  nn0ind-raph  10334  zindd  10335  rebtwnz  10537  qreccl  10558  xrlttri2  10699  xmulneg1  10812  iooshf  10953  difreicc  10992  elfznelfzo  11155  om2uzlti  11253  expcan  11395  hashvnfin  11605  hashgt0elex  11633  hashgt12el  11645  hashgt12el2  11646  hashbclem  11664  hashf1lem2  11668  absz  12079  iserex  12413  absdvdsb  12831  dvdsabsb  12832  dvdsadd  12851  sadadd2lem2  12925  smupvallem  12958  gcdass  13008  1nprm  13047  lubid  14402  latlem12  14470  odudlatb  14585  issubm2  14712  nsgacs  14939  cycsubg2  14940  gapm  15046  sscntz  15088  odval2  15152  lsmcntz  15274  dfprm2  16737  isopn2  17059  cmpsub  17425  connsub  17445  itg1mulc  19557  lhop1  19859  mdegleb  19948  lawcos  20619  leibpi  20743  ausisusgra  21341  usgraedg4  21367  usgraidx2v  21373  nbgraf1olem1  21412  nb3graprlem1  21421  nb3grapr  21423  nb3grapr2  21424  cusgrarn  21429  uvtx01vtx  21462  redwlk  21567  wlkdvspthlem  21568  wlkdvspth  21569  ubthlem1  22333  norm-i  22592  hoeq  23224  nmopgt0  23376  pjimai  23640  chirredi  23858  addltmulALT  23910  iunrdx  23975  disjrdx  23992  zmodid2  25075  relexpindlem  25100  prodrb  25219  nofulllem2  25579  colinearalg  25761  mbfresfi  26160  itg2addnclem  26163  itg2addnclem2  26164  itg2addnclem3  26165  topfne  26268  isidlc  26523  istopclsd  26652  eqrabdioph  26734  rexzrexnn0  26762  zindbi  26907  expdiophlem2  26991  islinds3  27180  f1omvdcnv  27263  pm14.122a  27498  2reu4a  27842  ralbinrald  27852  afvco2  27915  elfzomelpfzo  27997  swrd0swrd  28017  swrdswrd  28019  swrdccatin12lem3b  28030  swrdccatin12b  28035  el2spthonot0  28076  el2wlkonotot  28078  el2wlkonotot1  28079  el2wlksotot  28087  usg2wlkonot  28088  2pthwlkonot  28090  usg2spthonot  28093  usg2spthonot0  28094  frgrancvvdeqlemC  28150  frgraeu  28165  frg2woteq  28171  onfrALTlem5  28347  bitr3VD  28679  onfrALTlem5VD  28715  csbrngVD  28726  nfsb4twAUX7  29292  sbcoNEW7  29297  sbco2wAUX7  29300  sbco2OLD7  29448  islshpsm  29475  lshpkrlem1  29605  opcon1b  29693  lautlt  30585  lauteq  30589  idlaut  30590  diblsmopel  31666  doch11  31868
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