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

Theorem biimpd 207
Description: Deduce an implication from a logical equivalence. (Contributed by NM, 11-Jan-1993.)
Hypothesis
Ref Expression
biimpd.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
biimpd  |-  ( ph  ->  ( ps  ->  ch ) )

Proof of Theorem biimpd
StepHypRef Expression
1 biimpd.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
2 bi1 186 . 2  |-  ( ( ps  <->  ch )  ->  ( ps  ->  ch ) )
31, 2syl 16 1  |-  ( ph  ->  ( ps  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185
This theorem is referenced by:  mpbid  210  sylibd  214  sylbid  215  mpbidi  216  syl5ib  219  syl6bi  228  ibi  241  con4bid  293  mtbird  301  mtbiri  303  imbi1d  317  pm5.21im  349  biimpa  484  exintr  1689  spfw  1792  cbvalw  1794  alcomiw  1797  19.9d  1878  19.23t  1895  spimt  1991  spv  1997  chvar  1999  cbval  2007  nfsb4t  2116  dral1-o  2219  2eu3  2365  eqrdav  2441  eqrdavOLD  2442  cleqhOLD  2559  rgen2a  2870  ralcom2  3008  ceqsalgALT  3121  vtoclf  3146  vtocl2  3148  vtocl3  3149  spcdv  3178  rspcdv  3199  rexraleqim  3211  elabgt  3229  sbcn1  3361  sbcim1  3362  sbcbi1  3363  sbeqalb  3370  sbcel21v  3381  eqrd  3507  elpwunsn  4055  rabsnifsb  4083  ssunsn2  4174  euotd  4738  sotr2  4819  onmindif  4957  relop  5143  elres  5299  restidsing  5320  elimasni  5354  sotri2  5386  relcnvtr  5517  iotaval  5552  dffv2  5931  mpteqb  5955  elfvmptrab  5962  chfnrn  5983  elpreima  5992  iinpreima  6002  exfo  6034  ffnfv  6042  f1elima  6156  f1eqcocnv  6189  fliftfun  6195  soisores  6208  isotr  6217  isomin  6218  ovmpt2dv2  6421  difsnexi  6593  onint  6615  oneqmin  6625  ordunisuc2  6664  tfindsg  6680  findsg  6712  f1oweALT  6769  ressuppss  6921  funsssuppss  6928  imacosupp  6942  smoiso  7035  seqomlem2  7118  oaordi  7197  oawordri  7201  oaordex  7209  oalimcl  7211  omwordi  7222  oewordi  7242  oelim2  7246  nnmwordi  7286  xpider  7384  iiner  7385  undifixp  7507  mptelixpg  7508  dom2lem  7557  nneneq  7702  fineqvlem  7736  pssnn  7740  dif1enOLD  7754  dif1en  7755  findcard2s  7763  unfilem2  7787  xpfi  7793  domunfican  7795  fsuppimp  7837  dffi2  7885  wemaplem2  7975  suc11reg  8039  noinfep  8079  cantnflem1  8111  cantnflem1OLD  8134  r1fin  8194  tcrank  8305  cardlim  8356  pr2nelem  8385  fseqenlem1  8408  alephnbtwn  8455  alephord2i  8461  alephf1  8469  cardaleph  8473  alephiso  8482  dfac12lem2  8527  ackbij1lem16  8618  cflm  8633  cfcoflem  8655  sornom  8660  fin23lem27  8711  isf32lem7  8742  fin17  8777  fin1a2lem2  8784  fin1a2lem4  8786  fin1a2lem6  8788  fin1a2lem9  8791  axdc3lem2  8834  zorn2lem7  8885  uniimadom  8922  inar1  9156  grothomex  9210  addcanpi  9280  mulcanpi  9281  enqer  9302  genpcd  9387  genpnmax  9388  ltexprlem4  9420  reclem3pr  9430  reclem4pr  9431  suplem2pr  9434  axpre-ltadd  9547  axpre-sup  9549  ltletr  9679  00id  9758  mul0or  10195  prodgt02  10394  prodge02  10396  lemul1a  10402  mulgt1  10407  divgt0  10416  divge0  10417  ledivp1i  10477  ltdivp1i  10478  cju  10538  nnsub  10580  nominpos  10781  nn0n0n1ge2  10865  btwnnz  10945  uzindOLD  10963  suprfinzcl  10983  ublbneg  11175  zmax  11188  cnref1o  11224  ltsubrp  11260  ltaddrp  11261  xrltletr  11369  qbtwnre  11407  xltnegi  11424  iccsupr  11626  icoshft  11651  difreicc  11661  iccshftri  11664  iccshftli  11666  iccdili  11668  icccntri  11670  fzen  11712  fzm1  11767  elfzmlbmOLD  11793  fzofzim  11848  eluzgtdifelfzo  11857  injresinjlem  11904  injresinj  11905  flval2  11929  flval3  11930  modaddmodup  12029  fseqsupubi  12067  ssnn0fi  12073  mptnn0fsuppr  12084  sq01  12267  hashf1rn  12404  hashle00  12444  hashgt12el  12460  hashgt12el2  12461  hash2pr  12494  hash2prb  12496  hashtpg  12502  hash3tr  12508  swrdnd  12636  swrdsymbeq  12651  2swrd1eqwrdeq  12658  ccatopth2  12675  reuccats1lem  12684  swrdccatin2  12691  swrdccat  12697  swrdccat3a  12698  swrdccat3blem  12699  repsdf2  12729  repswsymball  12730  repswrevw  12737  cshweqrep  12768  cshw1  12769  2cshwcshw  12772  scshwfzeqfzo  12773  cshwcsh2id  12775  swrdco  12782  swrd2lsw  12869  2swrd2eqwrdeq  12870  wwlktovfo  12875  cjre  12951  o1lo1  13339  o1of2  13414  o1rlimmul  13420  zsum  13519  modfsummods  13586  reeff1  13732  dvds2lem  13873  muldvds1  13885  dvdscmulr  13889  dvdsmulcr  13890  divalglem8  13935  ndvdsadd  13943  gcdmultiple  14065  prmn2uzge3  14114  isprm6  14127  isprm5  14130  prmdvdsexpr  14134  divgcdodd  14137  phiprmpw  14183  modprm0  14207  pythagtriplem4  14220  pcz  14281  1arith  14322  cshwrepswhash1  14464  divsfval  14821  fthmon  15170  setcmon  15288  setcepi  15289  pltnle  15470  pltval3  15471  lublecllem  15492  latasym  15559  odupos  15639  mrelatglb  15688  mrelatlub  15690  cnvpsb  15717  isgrpid2  15960  ghmf1  16169  orbsta  16225  resscntz  16243  gsmsymgrfixlem1  16326  gsmsymgreqlem2  16330  mndodcongi  16441  odf1  16458  lsmss1  16558  lsmss2  16560  efgredeu  16644  cntzcmnss  16723  lt6abl  16771  ablfaclem3  17012  kerf1hrm  17266  lspsneq  17642  lspsneu  17643  lsmcv  17661  lidldvgen  17777  0ringnnzr  17791  domnmuln0  17821  opprdomn  17824  ply1scln0  18206  gsummoncoe1  18220  domnchr  18442  znf1o  18463  zntoslem  18468  znfld  18472  cygznlem2a  18479  cygznlem3  18481  islindf4  18746  uvcendim  18755  matvscl  18806  scmataddcl  18891  scmatsubcl  18892  scmatfo  18905  scmatghm  18908  maducoeval2  19015  slesolinv  19055  cramerimplem2  19059  cpmatelimp  19086  cpmatelimp2  19088  cpmatacl  19090  cpmatinvcl  19091  pm2mpf1  19173  cayhamlem1  19240  cayleyhamilton1  19266  0ntr  19445  islpi  19523  lmss  19672  cmpcld  19775  cmpfi  19781  bwthOLD  19784  1stcelcls  19835  comppfsc  19906  ptcnplem  19995  qtophmeo  20191  fbdmn0  20208  fbasrn  20258  elfm3  20324  fmfnfmlem4  20331  fclscf  20399  cnpfcf  20415  alexsubALTlem3  20422  tsmsresOLD  20518  tsmsres  20519  blval2  20951  nmoleub  21111  nmhmcn  21476  iscau4  21591  caussi  21609  cniccbdd  21746  ovoliunnul  21791  mbfinf  21945  itg2splitlem  22028  dvcn  22197  c1lip1  22271  c1lip3  22273  dvcnvrelem1  22291  ply1divex  22410  quotcan  22577  aannenlem1  22596  taylf  22628  ulmcaulem  22661  ulmcau  22662  reeff1o  22714  logccv  22916  logreclem  23022  isosctrlem2  23025  xrlimcnp  23170  rlimcxp  23175  ftalem7  23224  vmappw  23262  fsumvma  23360  dchreq  23405  dchrptlem1  23411  dchrsum  23416  bposlem7  23437  lgsqrlem2  23489  lgsdchr  23495  lgseisenlem2  23497  lgsquad2  23507  2sqlem6  23516  isperp2  23964  xmstrkgc  24061  brbtwn  24074  brcgr  24075  axcgrid  24091  axeuclidlem  24137  axeuclid  24138  uhgraeq12d  24179  usgrac  24223  usgraeq12d  24234  usgranloopv  24250  nbgraf1olem5  24317  iscusgra0  24329  cusgrasize2inds  24349  cusgrafilem3  24353  usgramaxsize  24359  iswlkg  24396  wlkcompim  24398  wlkcpr  24401  wlkonprop  24407  trlonprop  24416  0wlkon  24421  usgrnloop  24437  pthonprop  24451  spthonprp  24459  redwlk  24480  wlkdvspthlem  24481  usgra2wlkspthlem2  24492  fargshiftfv  24507  wwlknimp  24559  vfwlkniswwlkn  24578  usg2wlkeq  24580  wwlknred  24595  wwlknext  24596  wwlknextbi  24597  wwlkextwrd  24600  wwlkextinj  24602  wwlkextsur  24603  wwlkm1edg  24607  isclwlkg  24627  clwlkcompim  24636  0clwlk  24637  clwwlkn2  24647  clwlkisclwwlklem2a1  24651  clwlkisclwwlklem2a4  24656  clwlkisclwwlklem2a  24657  clwlkisclwwlklem1  24659  clwwlkf  24666  wwlkext2clwwlk  24675  clwwisshclwwlem1  24677  wlklenvclwlk  24711  clwlkfclwwlk  24716  el2spthonot  24742  usg2wotspth  24756  usg2spthonot  24760  usg2spthonot0  24761  rgraprop  24800  rusgraprop  24801  rusgraprop3  24815  frgranbnb  24892  frgrancvvdeqlem3  24904  frgrancvvdeqlem4  24905  frgrancvvdeqlem7  24908  frgrawopreglem2  24917  frgrawopreg  24921  frgregordn0  24942  clwwlkextfrlem1  24948  extwwlkfablem2  24950  numclwwlkun  24951  numclwwlkovf2ex  24958  numclwlk1lem2foa  24963  numclwlk1lem2f1  24966  numclwwlk8  24987  gxid  25147  opidonOLD  25196  opidon2OLD  25198  grpomndo  25220  elghomlem2OLD  25236  rngoueqz  25304  dvrunz  25307  rngoridfz  25309  hlipgt0  25702  ocin  26086  ocnel  26088  shmodsi  26179  pjmf1  26506  unopf1o  26707  staddi  27037  stadd3i  27039  mdi  27086  dmdmd  27091  dmdi  27093  dmdbr2  27094  dmdbr3  27096  dmdbr4  27097  dmdi4  27098  mdsl1i  27112  superpos  27145  cvbr4i  27158  atssma  27169  atcv1  27171  atomli  27173  chirredlem1  27181  addltmulALT  27237  bian1d  27238  ifeqeqx  27291  disjxpin  27319  suppss3  27422  fpwrelmap  27428  xrge0infss  27452  ogrpaddlt  27581  metider  27746  tpr2rico  27767  xrge0iifiso  27790  qqhcn  27845  qqhucn  27846  esumlub  27941  esumpinfval  27952  esumpinfsum  27956  ballotlemfc0  28304  ballotlemfcc  28305  erdsze2lem2  28521  zprod  29044  trpredrec  29296  poseq  29308  soseq  29309  sltval2  29391  sltres  29399  nodenselem7  29422  nodenselem8  29423  nodense  29424  nobndup  29435  nobnddown  29436  nofulllem5  29441  dfrdg4  29575  altopthsn  29586  btwncomim  29638  btwnexch3  29645  btwnexch2  29648  endofsegid  29710  onsuct0  29881  ordcmp  29887  nndivsub  29897  wl-equsal1i  29971  wl-ax11-lem10  30009  ltflcei  30018  sin2h  30020  cos2h  30021  tan2h  30022  heicant  30024  mblfinlem1  30026  mblfinlem2  30027  mblfinlem3  30028  mblfinlem4  30029  mbfresfi  30036  cnambfre  30038  dvtanlem  30039  ftc1anc  30073  dvasin  30078  areacirclem1  30082  areacirclem4  30085  areacirc  30087  opnrebl2  30114  nn0prpwlem  30115  brabg2  30181  fzmul  30208  fdc  30213  incsequz2  30217  isbnd2  30254  divrngidl  30400  rexrabdioph  30702  fphpdo  30726  icodiamlt  30731  irrapxlem3  30735  rmxypairf1o  30822  rmxycomplete  30828  zindbi  30857  lermxnn0  30863  ltrmy  30865  rmyeq0  30866  rmyeq  30867  lermy  30868  acongsym  30889  acongneg2  30890  wepwsolem  30962  radcnvrat  31171  nzss  31198  expgrowthi  31214  ordpss  31314  fzisoeu  31449  climinf  31520  stoweidlem7  31678  stoweidlem62  31733  2reu3  32031  ralbinrald  32042  funressnfv  32051  afv0fv0  32072  afv0nbfvbi  32074  afvfv0bi  32075  fnbrafvb  32077  afvres  32095  tz6.12-afv  32096  afvco2  32099  ndmaovcl  32126  f1dmvrnfibi  32150  zm1nn  32163  subsubelfzo0  32176  usgra2pth  32192  usgpredgv  32237  usgpredgvALT  32238  usgfis  32284  usgfisALT  32288  mgmpropd  32301  clintop  32369  isassintop  32371  lidldomn1  32437  uzlidlring  32445  2zrngnmlid2  32467  funcestrcsetclem8  32502  rngccatidOLD  32537  ringccatidOLD  32597  srhmsubc  32617  srhmsubcOLD  32636  ztprmneprm  32669  pgrpgt2nabl  32692  lindslinindimp2lem4  32797  lincresunit3  32817  bi23impib  32987  bi23imp13  32993  bitr3  33013  rspsbc2  33038  tratrb  33040  sbcim2g  33042  truniALT  33045  3impcombi  33347  tpid3gVD  33375  orbi1rVD  33381  sbc3orgVD  33384  rspsbc2VD  33388  tratrbVD  33394  sbcim2gVD  33408  sbcbiVD  33409  truniALTVD  33411  trintALTVD  33413  trintALT  33414  csbingVD  33417  csbsngVD  33426  csbxpgVD  33427  csbresgVD  33428  csbrngVD  33429  csbima12gALTVD  33430  csbunigVD  33431  csbfv12gALTVD  33432  relopabVD  33434  isosctrlem1ALT  33467  bnj517  33676  bj-cbvexw  33983  bj-cbv3tb  34019  bj-spimtv  34026  bj-spvv  34032  bj-chvarv  34034  bj-cbvalv  34044  bj-cleqh  34106  bj-equsal  34147  bj-ax8  34209  bj-vtoclf  34228  bj-snsetex  34269  bj-inftyexpiinj  34352  bj-finsumval0  34403  bj-bary1lem1  34420  bj-bary1  34421  lsatn0  34464  l1cvpat  34519  leat2  34759  atnle  34782  cvlcvr1  34804  cvrexchlem  34883  cvratlem  34885  cvrat  34886  atcvrj0  34892  atle  34900  snatpsubN  35214  linepsubN  35216  pmapsub  35232  lneq2at  35242  lncvrelatN  35245  2llnma3r  35252  cdlemblem  35257  paddasslem5  35288  poml4N  35417  lhpmcvr4N  35490  trlval2  35628  cdlemd6  35668  cdleme7ga  35713  cdleme25b  35820  cdleme29b  35841  cdleme35fnpq  35915  cdleme50f1  36009  cdlemf1  36027  cdlemg27b  36162  cdlemk28-3  36374  tendospcanN  36490  diaf11N  36516  dia2dimlem1  36531  dibf11N  36628  dihf11  36734  dihmeetlem1N  36757  dochvalr  36824  dochnel2  36859  dvh4dimlem  36910  dochsat0  36924  mapd1o  37115  hdmapf1oN  37335  hgmapval0  37362  hgmapf1oN  37373  hlhilhillem  37430  frege52c  37608  suprleubrd  37652  suprlubrd  37656
  Copyright terms: Public domain W3C validator