Theorem biimpd 219

Description: Deduce an implication from a logical equivalence. Deduction associated with biimp 205 and biimpi 206. (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

Step	Hyp	Ref	Expression
1		biimpd.1	. 2 |- ( ph -> ( ps <-> ch ) )
2		biimp 205	. 2 |- ( ( ps <-> ch ) -> ( ps -> ch ) )
3	1, 2	syl 17	1 |- ( ph -> ( ps -> ch ) )

Syntax hints:   -> wi 4   <-> wb 196

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 197

This theorem is referenced by:  mpbid  222  sylibd  229  sylbid  230  mpbidi  231  syl5ib  234  syl6bi  243  ibi  256  con4bid  307  mtbird  315  mtbiri  317  imbi1d  331  bitr3  342  pm5.21im  364  biimpa  501  alexbii  1760  exintr  1819  spfw  1965  spfwOLD  1966  cbvalw  1968  alcomiw  1971  stdpc5OLD  2077  cbvalv1  2175  spimt  2253  spv  2260  chvar  2262  cbval  2271  nfsb4t  2389  2eu3  2555  eqrdav  2621  rgen2a  2977  ralcom2  3104  raleleq  3156  ceqsalgALT  3231  vtoclf  3258  vtocl  3259  vtocl2  3261  vtocl3  3262  spcdv  3291  rspcdv  3312  rspcebdv  3314  rexraleqim  3328  elabgt  3347  sbcn1  3481  sbcim1  3482  sbcbi1  3483  sbeqalb  3488  sbcel21v  3497  eqrdOLD  3623  elpwunsn  4224  rabsnifsb  4257  ssunsn2  4359  preqr1g  4385  propeqop  4970  euotd  4975  sotr2  5064  relop  5272  elres  5435  restidsingOLD  5459  elimasni  5492  sotri2  5525  relcnvtr  5655  onmindif  5815  iotaval  5862  dffv2  6271  mpteqb  6299  elfvmptrab  6306  chfnrn  6328  elpreima  6337  iinpreima  6345  exfo  6377  ffnfv  6388  f1elima  6520  f1eqcocnv  6556  fliftfun  6562  soisores  6577  isotr  6586  isomin  6587  ovmpt2dv2  6794  difsnexi  6970  onint  6995  oneqmin  7005  ordunisuc2  7044  tfindsg  7060  findsg  7093  f1oweALT  7152  el2mpt2cl  7251  ressuppss  7314  funsssuppss  7321  imacosupp  7335  smoiso  7459  seqomlem2  7546  oaordi  7626  oawordri  7630  oaordex  7638  oalimcl  7640  omwordi  7651  oewordi  7671  oelim2  7675  nnmwordi  7715  xpider  7818  iiner  7819  undifixp  7944  mptelixpg  7945  dom2lem  7995  nneneq  8143  fineqvlem  8174  pssnn  8178  dif1en  8193  findcard2s  8201  unfilem2  8225  xpfi  8231  domunfican  8233  f1dmvrnfibi  8250  fsuppimp  8281  dffi2  8329  wemaplem2  8452  suc11reg  8516  noinfep  8557  cantnflem1  8586  r1fin  8636  tcrank  8747  cardlim  8798  pr2nelem  8827  fseqenlem1  8847  alephnbtwn  8894  alephord2i  8900  alephf1  8908  cardaleph  8912  alephiso  8921  dfac12lem2  8966  ackbij1lem16  9057  cflm  9072  cfcoflem  9094  sornom  9099  fin23lem27  9150  isf32lem7  9181  fin17  9216  fin1a2lem2  9223  fin1a2lem4  9225  fin1a2lem6  9227  fin1a2lem9  9230  axdc3lem2  9273  zorn2lem7  9324  uniimadom  9366  inar1  9597  grothomex  9651  addcanpi  9721  mulcanpi  9722  enqer  9743  genpcd  9828  genpnmax  9829  ltexprlem4  9861  reclem3pr  9871  reclem4pr  9872  suplem2pr  9875  axpre-ltadd  9988  axpre-sup  9990  ltletr  10129  00id  10211  addn0nid  10451  mul0or  10667  prodgt02  10869  prodge02  10871  lemul1a  10877  mulgt1  10882  divgt0  10891  divge0  10892  ledivp1i  10949  ltdivp1i  10950  cju  11016  nnsub  11059  nominpos  11269  nn0n0n1ge2  11358  btwnnz  11453  suprfinzcl  11492  ublbneg  11773  zmax  11785  cnref1o  11827  ltsubrp  11866  ltaddrp  11867  xrltletr  11988  qbtwnre  12030  xltnegi  12047  xnn0xadd0  12077  iccsupr  12266  icoshft  12294  difreicc  12304  iccshftri  12307  iccshftli  12309  iccdili  12311  icccntri  12313  fzen  12358  elfz1b  12409  fzofzim  12514  eluzgtdifelfzo  12529  elfzo1elm1fzo0  12569  injresinjlem  12588  injresinj  12589  flval2  12615  flval3  12616  modmuladdim  12713  modaddmodup  12733  addmodlteq  12745  fseqsupubi  12777  ssnn0fi  12784  mptnn0fsuppr  12799  sq01  12986  hashf1rn  13142  hashf1rnOLD  13143  hashgt12el  13210  hashgt12el2  13211  hash2pr  13251  hash2exprb  13253  hashge2el2difr  13263  hashtpg  13267  hash3tr  13272  lswlgt0cl  13356  ccatalpha  13375  2swrd1eqwrdeq  13454  ccatopth2  13471  reuccats1lem  13479  swrdccatin2  13487  swrdccat  13493  swrdccat3a  13494  swrdccat3blem  13495  repsdf2  13525  repswsymball  13526  repswrevw  13533  cshweqrep  13567  cshw1  13568  2cshwcshw  13571  scshwfzeqfzo  13572  cshwcsh2id  13574  swrdco  13583  swrd2lsw  13695  2swrd2eqwrdeq  13696  wwlktovfo  13701  cjre  13879  icodiamlt  14174  o1lo1  14268  o1of2  14343  o1rlimmul  14349  zsum  14449  modfsummods  14525  zprod  14667  reeff1  14850  dvds2lem  14994  muldvds1  15006  dvdscmulr  15010  dvdsmulcr  15011  dvdsdivcl  15038  mod2eq1n2dvds  15071  oddnn02np1  15072  divalglem8  15123  ndvdsadd  15134  zeqzmulgcd  15232  dfgcd2  15263  gcdmultiple  15269  absproddvds  15330  lcmftp  15349  coprmdvds  15366  isprm5  15419  divgcdodd  15422  isprm6  15426  prmdvdsexpr  15429  cncongrprm  15437  phiprmpw  15481  modprm0  15510  pythagtriplem4  15524  pcz  15585  difsqpwdvds  15591  1arith  15631  prmgaplem5  15759  prmgaplem6  15760  cshwrepswhash1  15809  divsfval  16207  catsubcat  16499  fthmon  16587  isinitoi  16653  istermoi  16654  iszeroi  16659  setcmon  16737  setcepi  16738  funcestrcsetclem8  16787  fthestrcsetc  16790  funcsetcestrclem8  16802  fthsetcestrc  16805  pltnle  16966  pltval3  16967  lublecllem  16988  latasym  17055  odupos  17135  mrelatglb  17184  mrelatlub  17186  cnvpsb  17213  isgrpid2  17458  ghmghmrn  17679  ghmf1  17689  orbsta  17746  resscntz  17764  gsmsymgrfixlem1  17847  gsmsymgreqlem2  17851  mndodcongi  17962  odf1  17979  lsmss1  18079  lsmss2  18081  efgredeu  18165  cntzcmnss  18246  lt6abl  18296  ablfaclem3  18486  ringinvnz1ne0  18592  kerf1hrm  18743  lspsneq  19122  lspsneu  19123  lsmcv  19141  lidldvgen  19255  0ringnnzr  19269  domnmuln0  19298  opprdomn  19301  ply1scln0  19661  gsummoncoe1  19674  domnchr  19880  znf1o  19900  zntoslem  19905  znfld  19909  cygznlem2a  19916  cygznlem3  19918  islindf4  20177  uvcendim  20186  matvscl  20237  scmataddcl  20322  scmatsubcl  20323  scmatfo  20336  scmatghm  20339  maducoeval2  20446  slesolinv  20486  cramerimplem2  20490  cpmatelimp  20517  cpmatelimp2  20519  cpmatacl  20521  cpmatinvcl  20522  pm2mpf1  20604  cayhamlem1  20671  cayleyhamilton1  20697  0ntr  20875  islpi  20953  lmss  21102  cmpcld  21205  cmpfi  21211  1stcelcls  21264  comppfsc  21335  ptcnplem  21424  qtophmeo  21620  fbdmn0  21638  fbasrn  21688  elfm3  21754  fmfnfmlem4  21761  fclscf  21829  cnpfcf  21845  alexsubALTlem3  21853  tsmsres  21947  blval2  22367  tnggrpr  22459  nmoleub  22535  nmhmcn  22920  ncvs1  22957  iscau4  23077  caussi  23095  cniccbdd  23230  ovoliunnul  23275  mbfinf  23432  itg2splitlem  23515  dvcn  23684  c1lip1  23760  c1lip3  23762  dvcnvrelem1  23780  ply1divex  23896  quotcan  24064  aannenlem1  24083  taylf  24115  ulmcaulem  24148  ulmcau  24149  reeff1o  24201  logccv  24409  logreclem  24500  isosctrlem2  24549  xrlimcnp  24695  rlimcxp  24700  ftalem7  24805  vmappw  24842  fsumvma  24938  dchreq  24983  dchrptlem1  24989  dchrsum  24994  bposlem7  25015  lgsqrlem2  25072  lgsdchr  25080  gausslemma2dlem1a  25090  lgseisenlem2  25101  lgsquad2  25111  2lgslem1b  25117  2sqlem6  25148  tgcgrcomimp  25372  isperp2  25610  xmstrkgc  25766  brbtwn  25779  brcgr  25780  axcgrid  25796  axeuclidlem  25842  axeuclid  25843  lpvtx  25963  upgrex  25987  upgrpredgv  26034  upgredgpr  26037  uhgr0v0e  26130  subgrprop  26165  fusgrfisbase  26220  edgnbusgreu  26269  nbusgredgeu0  26270  cusgredg  26320  structtocusgr  26342  cusgrsize2inds  26349  cusgrsize  26350  usgredgsscusgredg  26355  fusgrmaxsize  26360  uspgrloopvtxel  26412  umgr2v2e  26421  vtxdginducedm1fi  26440  finsumvtxdg2sstep  26445  rgrprop  26456  rusgrprop  26458  0uhgrrusgr  26474  rusgrpropedg  26480  ewlkprop  26499  upgrewlkle2  26502  wlkprop  26507  upgrwlkcompim  26539  uspgr2wlkeq  26542  wlklenvclwlk  26551  wlkonprop  26554  wlkres  26567  redwlk  26569  wlkdlem2  26580  wksonproplem  26601  usgr2trlspth  26657  usgr2pth  26660  pthdlem1  26662  crctcshwlkn0lem4  26705  wspthnonp  26744  wlkiswwlks2  26761  wwlksm1edg  26767  wlknewwlksn  26773  wwlksnred  26787  wwlksnext  26788  wwlksnextbi  26789  wwlksnextwrd  26792  wwlksnextinj  26794  wwlksnextsur  26795  umgr2wlk  26845  umgrwwlks2on  26850  elwspths2on  26853  usgr2wspthons3  26857  elwwlks2  26861  clwwlknp  26887  clwlkclwwlklem2a1  26893  clwlkclwwlklem2a4  26898  clwlkclwwlklem2a  26899  clwlkclwwlklem2  26901  clwwlks1loop  26908  umgrclwwlksge2  26912  clwwlksf  26915  wwlksext2clwwlk  26924  clwwisshclwwslemlem  26926  clwwnisshclwwsn  26930  clwlksfclwwlk  26962  vdn0conngrumgrv2  27056  frgrnbnb  27157  frgrncvvdeqlem2  27164  frgrncvvdeqlem3  27165  frgrncvvdeqlem6  27168  frgrwopreglem4a  27174  fusgr2wsp2nb  27198  frrusgrord0lem  27203  clwwlkextfrlem1  27208  clwwlksnwwlksn  27209  numclwwlkovf2exlem2  27212  numclwwlk8  27250  frgrreg  27252  hlipgt0  27770  ocin  28155  ocnel  28157  shmodsi  28248  pjmf1  28575  unopf1o  28775  staddi  29105  stadd3i  29107  mdi  29154  dmdmd  29159  dmdi  29161  dmdbr2  29162  dmdbr3  29164  dmdbr4  29165  dmdi4  29166  mdsl1i  29180  superpos  29213  cvbr4i  29226  atssma  29237  atcv1  29239  atomli  29241  chirredlem1  29249  addltmulALT  29305  bian1d  29306  ifeqeqx  29361  disjxpin  29401  suppss3  29502  fpwrelmap  29508  ogrpaddlt  29718  metider  29937  tpr2rico  29958  xrge0iifiso  29981  qqhcn  30035  qqhucn  30036  esumlub  30122  esumpinfval  30135  esumpinfsum  30139  ballotlemfc0  30554  ballotlemfcc  30555  ftc2re  30676  bnj517  30955  erdsze2lem2  31186  trpredrec  31738  poseq  31750  soseq  31751  sltval2  31809  sltres  31815  nodenselem8  31841  nodense  31842  noresle  31846  scutun12  31917  madeval2  31936  dfrdg4  32058  altopthsn  32068  btwncomim  32120  btwnexch3  32127  btwnexch2  32130  endofsegid  32192  opnrebl2  32316  nn0prpwlem  32317  onsuct0  32440  ordcmp  32446  nndivsub  32456  dnibndlem13  32480  bj-cbvexw  32664  bj-cbv3tb  32711  bj-spimtv  32718  bj-spvv  32723  bj-chvarv  32725  bj-equsal  32813  bj-sbsb  32824  bj-ax8  32887  bj-vtoclf  32908  bj-snsetex  32951  bj-ismooredr2  33065  bj-inftyexpiinj  33096  bj-finsumval0  33147  bj-bary1lem1  33161  bj-bary1  33162  f1omptsnlem  33183  iooelexlt  33210  relowlpssretop  33212  rdgeqoa  33218  finxpsuclem  33234  wl-equsal1i  33329  wl-ax11-lem10  33371  ltflcei  33397  sin2h  33399  cos2h  33400  tan2h  33401  lindsenlbs  33404  matunitlindf  33407  poimirlem3  33412  poimirlem4  33413  poimirlem18  33427  poimirlem20  33429  poimirlem21  33430  poimirlem22  33431  poimirlem24  33433  poimirlem25  33434  poimirlem26  33435  poimirlem27  33436  poimirlem28  33437  poimirlem31  33440  poimir  33442  heicant  33444  mblfinlem1  33446  mblfinlem2  33447  mblfinlem3  33448  mblfinlem4  33449  mbfresfi  33456  cnambfre  33458  ftc1anc  33493  dvasin  33496  areacirclem1  33500  areacirclem4  33503  areacirc  33505  brabg2  33510  fzmul  33537  fdc  33541  incsequz2  33545  isbnd2  33582  opidonOLD  33651  opidon2OLD  33653  grpomndo  33674  elghomlem2OLD  33685  rngoueqz  33739  dvrunz  33753  divrngidl  33827  dral1-o  34189  lsatn0  34286  l1cvpat  34341  leat2  34581  atnle  34604  cvlcvr1  34626  cvrexchlem  34705  cvratlem  34707  cvrat  34708  atcvrj0  34714  atle  34722  snatpsubN  35036  linepsubN  35038  pmapsub  35054  lneq2at  35064  lncvrelatN  35067  2llnma3r  35074  cdlemblem  35079  paddasslem5  35110  poml4N  35239  lhpmcvr4N  35312  trlval2  35450  cdlemd6  35490  cdleme7ga  35535  cdleme25b  35642  cdleme29b  35663  cdleme35fnpq  35737  cdleme50f1  35831  cdlemf1  35849  cdlemg27b  35984  cdlemk28-3  36196  tendospcanN  36312  diaf11N  36338  dia2dimlem1  36353  dibf11N  36450  dihf11  36556  dihmeetlem1N  36579  dochvalr  36646  dochnel2  36681  dvh4dimlem  36732  dochsat0  36746  mapd1o  36937  hdmapf1oN  37157  hgmapval0  37184  hgmapf1oN  37195  hlhilhillem  37252  rexrabdioph  37358  fphpdo  37381  irrapxlem3  37388  rmxypairf1o  37476  rmxycomplete  37482  zindbi  37511  lermxnn0  37517  ltrmy  37519  rmyeq0  37520  rmyeq  37521  lermy  37522  acongsym  37543  acongneg2  37544  wepwsolem  37612  intabssd  37916  ss2iundf  37951  frege129d  38055  frege133d  38057  axfrege52a  38150  axfrege52c  38181  ntrk0kbimka  38337  gneispace  38432  suprleubrd  38466  suprlubrd  38470  radcnvrat  38513  nzss  38516  expgrowthi  38532  ordpss  38655  bi23impib  38691  bi23imp13  38697  rspsbc2  38744  tratrb  38746  sbcim2g  38748  truniALT  38751  3impcombi  39044  tpid3gVD  39077  orbi1rVD  39083  sbc3orgVD  39086  rspsbc2VD  39090  tratrbVD  39097  sbcim2gVD  39111  sbcbiVD  39112  truniALTVD  39114  trintALTVD  39116  trintALT  39117  csbingVD  39120  csbsngVD  39129  csbxpgVD  39130  csbresgVD  39131  csbrngVD  39132  csbima12gALTVD  39133  csbunigVD  39134  csbfv12gALTVD  39135  relopabVD  39137  isosctrlem1ALT  39170  fzisoeu  39514  xrralrecnnge  39613  allbutfi  39616  climinf  39838  liminfreuzlem  40034  climliminf  40038  climliminflimsup  40040  xlimbr  40053  stoweidlem7  40224  stoweidlem62  40279  sge0gerpmpt  40619  meaiuninclem  40697  carageniuncllem2  40736  issmflem  40936  2reu3  41188  ralbinrald  41199  funressnfv  41208  afv0fv0  41229  afv0nbfvbi  41231  afvfv0bi  41232  fnbrafvb  41234  afvres  41252  tz6.12-afv  41253  afvco2  41256  ndmaovcl  41283  nelbrim  41292  zm1nn  41316  nltle2tri  41323  subsubelfzo0  41336  iccpartres  41354  iccpartiltu  41358  fargshiftfv  41375  pfxfv  41399  pfxsuff1eqwrdeq  41407  reuccatpfxs1lem  41433  fmtnof1  41447  goldbachthlem2  41458  fmtnoprmfac1  41477  fmtnoprmfac2  41479  lighneallem2  41523  lighneallem4b  41526  lighneallem4  41527  evennodd  41556  oddneven  41557  oexpnegALTV  41588  oexpnegnz  41589  evenltle  41626  gbowge7  41651  gbege6  41653  sbgoldbwt  41665  sbgoldbst  41666  nnsum3primesle9  41682  bgoldbtbndlem2  41694  prsprel  41737  sprsymrelf1lem  41741  sprsymrelfolem2  41743  sprsymrelfo  41747  mgmpropd  41775  clintop  41844  isassintop  41846  lidldomn1  41921  uzlidlring  41929  2zrngnmlid2  41951  rngccatidALTV  41989  ringccatidALTV  42052  srhmsubc  42076  srhmsubcALTV  42094  ztprmneprm  42125  pgrpgt2nabl  42147  lindslinindimp2lem4  42250  lincresunit3  42270  fldivexpfllog2  42359  digexp  42401  spd  42425  spcdvw  42426  setrec2fun  42439