MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bicomd Structured version   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  1377  cad1  1407  sbequ12r  1945  sbco  2158  sbco2  2161  cbvab  2553  necon3bbid  2632  necon4bbid  2663  ralcom2  2864  gencbvex  2990  sbhypf  2993  clel3g  3065  reu8  3122  sbceq2a  3164  sbcco2  3176  r19.9rzv  3714  sbcsng  3857  disjxun  4202  opabid  4453  soeq2  4515  ordintdif  4622  tfisi  4830  tfinds2  4835  posn  4938  xpiindi  5002  fvopab6  5818  fconstfv  5946  cbvfo  6014  f1eqcocnv  6020  isoid  6041  isoini  6050  isosolem  6059  f1oweALT  6066  resoprab2  6159  dfoprab3  6395  opiota  6527  tfrlem5  6633  oalimcl  6795  omword  6805  oeword  6825  nnacan  6863  nnmcan  6869  findcard2s  7341  brwdomn0  7529  ssrankr1  7753  r1pw  7763  aleph11  7957  alephval3  7983  gch-kn  8548  wunex2  8605  lttri2  9149  wloglei  9551  divne0b  9681  lemul1  9854  nn0ind-raph  10362  zindd  10363  rebtwnz  10565  qreccl  10586  xrlttri2  10727  xmulneg1  10840  iooshf  10981  difreicc  11020  elfznelfzo  11184  om2uzlti  11282  expcan  11424  hashvnfin  11634  hashgt0elex  11662  hashgt12el  11674  hashgt12el2  11675  hashbclem  11693  hashf1lem2  11697  absz  12108  iserex  12442  absdvdsb  12860  dvdsabsb  12861  dvdsadd  12880  sadadd2lem2  12954  smupvallem  12987  gcdass  13037  1nprm  13076  lubid  14431  latlem12  14499  odudlatb  14614  issubm2  14741  nsgacs  14968  cycsubg2  14969  gapm  15075  sscntz  15117  odval2  15181  lsmcntz  15303  dfprm2  16766  isopn2  17088  cmpsub  17455  connsub  17476  itg1mulc  19588  lhop1  19890  mdegleb  19979  lawcos  20650  leibpi  20774  ausisusgra  21372  usgraedg4  21398  usgraidx2v  21404  nbgraf1olem1  21443  nb3graprlem1  21452  nb3grapr  21454  nb3grapr2  21455  cusgrarn  21460  uvtx01vtx  21493  redwlk  21598  wlkdvspthlem  21599  wlkdvspth  21600  ubthlem1  22364  norm-i  22623  hoeq  23255  nmopgt0  23407  pjimai  23671  chirredi  23889  addltmulALT  23941  iunrdx  24006  disjrdx  24023  zmodid2  25106  relexpindlem  25131  prodrb  25250  nofulllem2  25650  colinearalg  25841  mbfresfi  26243  itg2addnclem  26246  itg2addnclem2  26247  itg2addnclem3  26248  ftc1anclem1  26270  topfne  26361  isidlc  26616  istopclsd  26745  eqrabdioph  26827  rexzrexnn0  26855  zindbi  27000  expdiophlem2  27084  islinds3  27272  f1omvdcnv  27355  pm14.122a  27590  2reu4a  27934  ralbinrald  27944  afvco2  28007  elfzomelpfzo  28112  subsubelfzo0  28118  2submod  28130  swrd0swrd  28163  swrdswrd  28165  swrdccat3  28181  cshwidxmod  28209  2cshw2lem2  28219  2cshwmod  28223  el2spthonot0  28291  el2wlkonotot  28293  el2wlkonotot1  28294  el2wlksotot  28302  usg2wlkonot  28303  2pthwlkonot  28305  usg2spthonot  28308  usg2spthonot0  28309  frgrancvvdeqlemC  28365  frgraeu  28380  frg2woteq  28386  onfrALTlem5  28565  bitr3VD  28898  onfrALTlem5VD  28934  csbrngVD  28945  nfsb4twAUX7  29513  sbcoNEW7  29519  sbco2wAUX7  29522  sbco2OLD7  29689  islshpsm  29715  lshpkrlem1  29845  opcon1b  29933  lautlt  30825  lauteq  30829  idlaut  30830  diblsmopel  31906  doch11  32108
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