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  2132  sbco2  2135  cbvab  2522  necon3bbid  2601  necon4bbid  2632  ralcom2  2832  gencbvex  2958  sbhypf  2961  clel3g  3033  reu8  3090  sbceq2a  3132  sbcco2  3144  r19.9rzv  3682  sbcsng  3825  disjxun  4170  opabid  4421  soeq2  4483  ordintdif  4590  tfisi  4797  tfinds2  4802  posn  4905  xpiindi  4969  fvopab6  5785  fconstfv  5913  cbvfo  5981  f1eqcocnv  5987  isoid  6008  isoini  6017  isosolem  6026  f1oweALT  6033  resoprab2  6126  dfoprab3  6362  opiota  6494  tfrlem5  6600  oalimcl  6762  omword  6772  oeword  6792  nnacan  6830  nnmcan  6836  findcard2s  7308  brwdomn0  7493  ssrankr1  7717  r1pw  7727  aleph11  7921  alephval3  7947  gch-kn  8512  wunex2  8569  lttri2  9113  wloglei  9515  divne0b  9645  lemul1  9818  nn0ind-raph  10326  zindd  10327  rebtwnz  10529  qreccl  10550  xrlttri2  10691  xmulneg1  10804  iooshf  10945  difreicc  10984  elfznelfzo  11147  om2uzlti  11245  expcan  11387  hashvnfin  11597  hashgt0elex  11625  hashgt12el  11637  hashgt12el2  11638  hashbclem  11656  hashf1lem2  11660  absz  12071  iserex  12405  absdvdsb  12823  dvdsabsb  12824  dvdsadd  12843  sadadd2lem2  12917  smupvallem  12950  gcdass  13000  1nprm  13039  lubid  14394  latlem12  14462  odudlatb  14577  issubm2  14704  nsgacs  14931  cycsubg2  14932  gapm  15038  sscntz  15080  odval2  15144  lsmcntz  15266  dfprm2  16729  isopn2  17051  cmpsub  17417  connsub  17437  itg1mulc  19549  lhop1  19851  mdegleb  19940  lawcos  20611  leibpi  20735  ausisusgra  21333  usgraedg4  21359  usgraidx2v  21365  nbgraf1olem1  21404  nb3graprlem1  21413  nb3grapr  21415  nb3grapr2  21416  cusgrarn  21421  uvtx01vtx  21454  redwlk  21559  wlkdvspthlem  21560  wlkdvspth  21561  ubthlem1  22325  norm-i  22584  hoeq  23216  nmopgt0  23368  pjimai  23632  chirredi  23850  addltmulALT  23902  iunrdx  23967  disjrdx  23984  zmodid2  25067  relexpindlem  25092  prodrb  25211  nofulllem2  25571  colinearalg  25753  mbfresfi  26152  itg2addnclem  26155  itg2addnclem2  26156  itg2addnclem3  26157  topfne  26260  isidlc  26515  istopclsd  26644  eqrabdioph  26726  rexzrexnn0  26754  zindbi  26899  expdiophlem2  26983  islinds3  27172  f1omvdcnv  27255  pm14.122a  27490  2reu4a  27834  ralbinrald  27844  afvco2  27907  elfzomelpfzo  27989  swrd0swrd  28009  swrdswrd  28011  swrdccatin12lem3b  28022  swrdccatin12b  28027  el2spthonot0  28068  el2wlkonotot  28070  el2wlkonotot1  28071  el2wlksotot  28079  usg2wlkonot  28080  2pthwlkonot  28082  usg2spthonot  28085  usg2spthonot0  28086  frgrancvvdeqlemC  28142  frgraeu  28157  frg2woteq  28163  onfrALTlem5  28339  bitr3VD  28670  onfrALTlem5VD  28706  csbrngVD  28717  nfsb4twAUX7  29280  sbcoNEW7  29285  sbco2wAUX7  29288  sbco2OLD7  29436  islshpsm  29463  lshpkrlem1  29593  opcon1b  29681  lautlt  30573  lauteq  30577  idlaut  30578  diblsmopel  31654  doch11  31856
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