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

Theorem bicomd 192
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 191 . 2  |-  ( ( ps  <->  ch )  <->  ( ch  <->  ps ) )
31, 2sylib 188 1  |-  ( ph  ->  ( ch  <->  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  impbid2  195  syl5ibr  212  ibir  233  bitr2d  245  bitr3d  246  bitr4d  247  syl5rbb  249  syl6rbb  253  con1bid  320  pm5.5  326  anabs5  784  pm5.55  867  pm5.54  870  baibr  872  baibd  875  rbaibd  876  pm5.75  903  ninba  927  3impexpbicomi  1358  cad1  1388  sbequ12r  1861  sbco  2023  sbco2  2026  cbvab  2401  necon3bbid  2480  necon4bbid  2511  ralcom2  2704  gencbvex  2830  sbhypf  2833  clel3g  2905  reu8  2961  sbceq2a  3002  sbcco2  3014  r19.9rzv  3548  sbcsng  3690  disjxun  4021  opabid  4271  soeq2  4334  ordintdif  4441  tfisi  4649  tfinds2  4654  posn  4758  xpiindi  4821  fvopab6  5621  fconstfv  5734  cbvfo  5799  f1eqcocnv  5805  isoid  5826  isoini  5835  isosolem  5844  f1oweALT  5851  resoprab2  5941  dfoprab3  6176  opiota  6290  tfrlem5  6396  oalimcl  6558  omword  6568  oeword  6588  nnacan  6626  nnmcan  6632  findcard2s  7099  brwdomn0  7283  ssrankr1  7507  r1pw  7517  aleph11  7711  alephval3  7737  gch-kn  8303  wunex2  8360  lttri2  8904  wloglei  9305  divne0b  9435  lemul1  9608  nn0ind-raph  10112  zindd  10113  rebtwnz  10315  qreccl  10336  xrlttri2  10476  xmulneg1  10589  iooshf  10728  difreicc  10767  om2uzlti  11013  expcan  11154  hashbclem  11390  hashf1lem2  11394  absz  11796  iserex  12130  absdvdsb  12547  dvdsabsb  12548  dvdsadd  12567  sadadd2lem2  12641  smupvallem  12674  gcdass  12724  1nprm  12763  lubid  14116  latlem12  14184  odudlatb  14299  issubm2  14426  nsgacs  14653  cycsubg2  14654  gapm  14760  sscntz  14802  odval2  14866  lsmcntz  14988  dfprm2  16447  isopn2  16769  cmpsub  17127  connsub  17147  itg1mulc  19059  lhop1  19361  mdegleb  19450  lawcos  20114  leibpi  20238  ubthlem1  21449  norm-i  21708  hoeq  22340  nmopgt0  22492  pjimai  22756  chirredi  22974  addltmulALT  23026  iunrdx  23161  disjrdx  23370  zmodid2  24010  relexpindlem  24036  nofulllem2  24357  colinearalg  24538  eqintg  24961  splint  25048  cnvref  25065  domtri3  25105  domintrefc  25125  mnlmxl2  25269  nelioo5  25511  intopcoaconb  25540  cmptdst  25568  lvsovso2  25627  supnuf  25629  supexr  25631  isfuna  25834  idcatfun  25941  clscnc  26010  pdiveql  26168  topfne  26290  raleqfnOLD  26357  fdc  26455  isidlc  26640  bicomddOLD  26706  istopclsd  26775  eqrabdioph  26857  rexzrexnn0  26885  zindbi  27031  expdiophlem2  27115  islinds3  27304  f1omvdcnv  27387  pm14.122a  27622  stoweidlem13  27762  2reu4a  27967  ralbinrald  27977  afvco2  28037  uvtx01vtx  28164  onfrALTlem5  28307  bitr3VD  28625  onfrALTlem5VD  28661  csbrngVD  28672  islshpsm  29170  lshpkrlem1  29300  opcon1b  29388  lautlt  30280  lauteq  30284  idlaut  30285  diblsmopel  31361  doch11  31563
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 177
  Copyright terms: Public domain W3C validator