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  1873  sbco  2036  sbco2  2039  cbvab  2414  necon3bbid  2493  necon4bbid  2524  ralcom2  2717  gencbvex  2843  sbhypf  2846  clel3g  2918  reu8  2974  sbceq2a  3015  sbcco2  3027  r19.9rzv  3561  sbcsng  3703  disjxun  4037  opabid  4287  soeq2  4350  ordintdif  4457  tfisi  4665  tfinds2  4670  posn  4774  xpiindi  4837  fvopab6  5637  fconstfv  5750  cbvfo  5815  f1eqcocnv  5821  isoid  5842  isoini  5851  isosolem  5860  f1oweALT  5867  resoprab2  5957  dfoprab3  6192  opiota  6306  tfrlem5  6412  oalimcl  6574  omword  6584  oeword  6604  nnacan  6642  nnmcan  6648  findcard2s  7115  brwdomn0  7299  ssrankr1  7523  r1pw  7533  aleph11  7727  alephval3  7753  gch-kn  8319  wunex2  8376  lttri2  8920  wloglei  9321  divne0b  9451  lemul1  9624  nn0ind-raph  10128  zindd  10129  rebtwnz  10331  qreccl  10352  xrlttri2  10492  xmulneg1  10605  iooshf  10744  difreicc  10783  om2uzlti  11029  expcan  11170  hashbclem  11406  hashf1lem2  11410  absz  11812  iserex  12146  absdvdsb  12563  dvdsabsb  12564  dvdsadd  12583  sadadd2lem2  12657  smupvallem  12690  gcdass  12740  1nprm  12779  lubid  14132  latlem12  14200  odudlatb  14315  issubm2  14442  nsgacs  14669  cycsubg2  14670  gapm  14776  sscntz  14818  odval2  14882  lsmcntz  15004  dfprm2  16463  isopn2  16785  cmpsub  17143  connsub  17163  itg1mulc  19075  lhop1  19377  mdegleb  19466  lawcos  20130  leibpi  20254  ubthlem1  21465  norm-i  21724  hoeq  22356  nmopgt0  22508  pjimai  22772  chirredi  22990  addltmulALT  23042  iunrdx  23177  disjrdx  23385  zmodid2  24025  relexpindlem  24051  prodrb  24155  nofulllem2  24428  colinearalg  24610  itg2addnclem  25003  itg2addnclem2  25004  itg2addnc  25005  eqintg  25064  splint  25151  cnvref  25168  domtri3  25208  domintrefc  25228  mnlmxl2  25372  nelioo5  25614  intopcoaconb  25643  cmptdst  25671  lvsovso2  25730  supnuf  25732  supexr  25734  isfuna  25937  idcatfun  26044  clscnc  26113  pdiveql  26271  topfne  26393  raleqfnOLD  26460  fdc  26558  isidlc  26743  bicomddOLD  26809  istopclsd  26878  eqrabdioph  26960  rexzrexnn0  26988  zindbi  27134  expdiophlem2  27218  islinds3  27407  f1omvdcnv  27490  pm14.122a  27725  stoweidlem13  27865  2reu4a  28070  ralbinrald  28080  afvco2  28144  elfznelfzo  28213  hashgt12el  28218  hashgt12el2  28219  nb3graprlem1  28287  nb3grapr  28289  nb3grapr2  28290  uvtx01vtx  28305  redwlk  28364  wlkdvspthlem  28365  wlkdvspth  28366  onfrALTlem5  28606  bitr3VD  28941  onfrALTlem5VD  28977  csbrngVD  28988  nfsb4twAUX7  29551  sbcoNEW7  29556  sbco2wAUX7  29559  sbco2OLD7  29706  islshpsm  29792  lshpkrlem1  29922  opcon1b  30010  lautlt  30902  lauteq  30906  idlaut  30907  diblsmopel  31983  doch11  32185
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