Theorem biimpd 144

Description: Deduce an implication from a logical equivalence. (Contributed by NM, 5-Aug-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 118	. 2 |- ( ( ps <-> ch ) -> ( ps -> ch ) )
3	1, 2	syl 14	1 |- ( ph -> ( ps -> ch ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used by:  mpbid  147  sylibd  149  sylbid  150  mpbidi  151  imbitrid  154  biimtrdi  163  ibi  176  imbi1d  231  biimpa  296  mtbird  684  mtbiri  686  orbi2d  802  pm5.15dc  1438  exlimd2  1648  exintr  1687  19.9d  1713  19.23t  1729  chvarfv  1752  dral1  1783  spimt  1789  cbvalv1  1804  cbvalh  1806  chvar  1810  exdistrfor  1853  sbequi  1892  spv  1913  cbvexvw  1976  eqrdav  2237  cleqh  2338  ceqsalg  2850  vtoclf  2876  vtocl2  2878  vtocl3  2879  spcdv  2910  rspcdv  2932  elabgt  2967  sbcn1  3099  sbcim1  3100  sbcbi1  3101  sbeqalb  3108  sbcel21v  3116  eqrd  3266  ifeqeqxdc  3687  rabsnifsb  3777  exmidsssn  4341  exmidsssnc  4342  copsexg  4386  euotd  4397  rexxfrd  4611  relop  4932  reldmm  5002  elres  5101  rnxpid  5225  relcnvtr  5310  iotaval  5352  mpteqb  5799  elfvmptrab  5805  chfnrn  5823  elpreima  5831  ffnfv  5869  f1elima  5982  f1eqcocnv  6000  fliftfun  6005  isoresbr  6018  isotr  6025  ovmpodv2  6225  ressuppss  6498  funsssuppss  6502  smoiso  6577  nnaordi  6785  nnaword  6788  nnawordi  6792  xpider  6884  iinerm  6885  mptelixpg  7020  dom2lem  7062  nneneq  7162  exmidpw  7219  infidc  7252  f1dmvrnfibi  7262  fsuppimp  7297  ismkvnex  7501  pr2nelem  7543  exmidfodomrlemeldju  7557  exmidfodomrlemreseldju  7558  netap  7626  2omotaplemap  7629  addcanpig  7707  mulcanpig  7708  enqer  7731  ltexnqi  7782  prarloclemlo  7867  genpcdl  7892  genpcuu  7893  appdivnq  7936  ltprordil  7962  1idprl  7963  1idpru  7964  ltexprlemm  7973  ltexprlemopu  7976  ltexprlemru  7985  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  caucvgprprlemopu  8072  caucvgsrlemoffcau  8171  caucvgsrlemoffres  8173  ltrenn  8228  axpre-ltadd  8259  addn0nid  8707  apne  8959  aptap  8986  prodgt02  9191  prodge02  9193  mulgt1  9201  divgt0  9210  divge0  9211  cju  9299  nnsub  9352  nominpos  9554  zltnle  9701  nn0n0n1ge2  9726  zdcle  9732  btwnnz  9751  uzm1  9969  supinfneg  10011  infsupneg  10012  ublbneg  10029  cnref1o  10068  ltsubrp  10108  ltaddrp  10109  xnn0dcle  10221  npnflt  10234  nmnfgt  10237  ge0nemnf  10243  xltnegi  10254  xnn0xadd0  10286  iccsupr  10385  icoshft  10409  iccshftri  10414  iccshftli  10416  iccdili  10418  icccntri  10420  fzdcel  10461  fznlem  10462  fzen  10464  fzofzim  10617  eluzgtdifelfzo  10632  elfzonelfzo  10665  qltnle  10695  addmodlteq  10856  qsqeqor  11108  apexp1  11178  fihashf1rn  11249  lswlgt0cl  11379  ccatalpha  11403  pfxfv  11478  pfxsuff1eqwrdeq  11493  ccatopth2  11511  swrdccat  11529  swrdccat3blem  11533  reuccatpfxs1lem  11540  cjre  11669  caucvgre  11769  icodiamlt  11969  zsumdc  12176  zproddc  12371  reeff1  12492  dvdsmod0  12585  dvds2lem  12595  muldvds1  12608  dvdscmulr  12612  dvdsmulcr  12613  dvdsdivcl  12642  oddnn02np1  12672  ndvdsadd  12723  bitsinv1lem  12753  zeqzmulgcd  12772  bezoutlemmain  12800  dfgcd2  12816  gcdmultiple  12822  coprmdvds  12895  divgcdodd  12947  isprm6  12951  prmdvdsexpr  12954  cncongrprm  12961  phiprmpw  13029  modprm0  13062  pythagtriplem4  13076  pcz  13140  difsqpwdvds  13146  pcadd  13148  1arith  13175  ballotfilemfc0  13290  ballotfilemfcc  13291  isgrpid2  13904  ghmghmrn  14125  ghmf1  14135  kerf1ghm  14136  imasabl  14230  rng1zrlem  14365  ringinvnz1ne0  14461  subrngringnsg  14622  domnmuln0  14691  rnglidlmcl  14926  znf1o  15095  znidom  15101  lmss  15472  cnplimcim  15893  dvcn  15926  fsumdvdsmul  16285  bposlem7  16317  gausslemma2dlem1a  16382  lgseisenlem2  16395  lgsquad2  16407  2lgslem1b  16413  2sqlem6  16444  upgrpredgv  16592  upgredgpr  16595  uhgr0v0e  16680  subgrprop  16705  wlkpropg  16770  upgrwlkcompim  16808  uspgr2wlkeq  16811  wlklenvclwlk  16819  wlkres  16825  clwwlk1loop  16845  umgrclwwlkge2  16848  clwwlkn1loopb  16866  clwwlknonex2lem2  16884  ch2var  17000  bj-rspgt  17019  bj-charfundcALT  17040  bj-nntrans  17182  bj-nnelirr  17184  bj-omtrans  17187  setindft  17196  bj-inf2vnlem3  17203  bj-inf2vnlem4  17204  bj-findis  17210  pw1nct  17238