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 ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpbid  147  sylibd  149  sylbid  150  mpbidi  151  imbitrid  154  biimtrdi  163  ibi  176  imbi1d  231  biimpa  296  mtbird  680  mtbiri  682  orbi2d  798  pm5.15dc  1434  exlimd2  1644  exintr  1683  19.9d  1709  19.23t  1725  chvarfv  1748  dral1  1779  spimt  1785  cbvalv1  1800  cbvalh  1802  chvar  1806  exdistrfor  1849  sbequi  1888  spv  1909  cbvexvw  1972  eqrdav  2233  cleqh  2334  ceqsalg  2844  vtoclf  2870  vtocl2  2872  vtocl3  2873  spcdv  2904  rspcdv  2926  elabgt  2960  sbcn1  3092  sbcim1  3093  sbcbi1  3094  sbeqalb  3101  sbcel21v  3109  eqrd  3258  rabsnifsb  3759  exmidsssn  4317  exmidsssnc  4318  copsexg  4362  euotd  4373  rexxfrd  4586  relop  4907  reldmm  4977  elres  5076  rnxpid  5199  relcnvtr  5284  iotaval  5326  mpteqb  5770  elfvmptrab  5775  chfnrn  5791  elpreima  5799  ffnfv  5837  f1elima  5948  f1eqcocnv  5966  fliftfun  5971  isoresbr  5984  isotr  5991  ovmpodv2  6189  ressuppss  6456  funsssuppss  6460  smoiso  6535  nnaordi  6743  nnaword  6746  nnawordi  6750  xpider  6842  iinerm  6843  mptelixpg  6971  dom2lem  7013  nneneq  7113  exmidpw  7170  infidc  7203  f1dmvrnfibi  7213  fsuppimp  7247  ismkvnex  7448  pr2nelem  7490  exmidfodomrlemeldju  7504  exmidfodomrlemreseldju  7505  netap  7570  2omotaplemap  7573  addcanpig  7651  mulcanpig  7652  enqer  7675  ltexnqi  7726  prarloclemlo  7811  genpcdl  7836  genpcuu  7837  appdivnq  7880  ltprordil  7906  1idprl  7907  1idpru  7908  ltexprlemm  7917  ltexprlemopu  7920  ltexprlemru  7929  cauappcvgprlemladdru  7973  cauappcvgprlemladdrl  7974  caucvgprprlemopu  8016  caucvgsrlemoffcau  8115  caucvgsrlemoffres  8117  ltrenn  8172  axpre-ltadd  8203  addn0nid  8649  apne  8899  aptap  8926  prodgt02  9129  prodge02  9131  mulgt1  9139  divgt0  9148  divge0  9149  cju  9237  nnsub  9278  nominpos  9478  zltnle  9625  nn0n0n1ge2  9650  zdcle  9656  btwnnz  9675  uzm1  9888  supinfneg  9930  infsupneg  9931  ublbneg  9948  cnref1o  9986  ltsubrp  10026  ltaddrp  10027  xnn0dcle  10138  npnflt  10151  nmnfgt  10154  ge0nemnf  10160  xltnegi  10171  xnn0xadd0  10203  iccsupr  10302  icoshft  10326  iccshftri  10331  iccshftli  10333  iccdili  10335  icccntri  10337  fzdcel  10377  fznlem  10378  fzen  10380  fzofzim  10531  eluzgtdifelfzo  10546  elfzonelfzo  10579  qltnle  10607  addmodlteq  10764  qsqeqor  11016  apexp1  11084  fihashf1rn  11155  lswlgt0cl  11281  ccatalpha  11305  pfxfv  11380  pfxsuff1eqwrdeq  11395  ccatopth2  11413  swrdccat  11431  swrdccat3blem  11435  reuccatpfxs1lem  11442  cjre  11571  caucvgre  11670  icodiamlt  11869  zsumdc  12074  zproddc  12269  reeff1  12390  dvdsmod0  12483  dvds2lem  12493  muldvds1  12506  dvdscmulr  12510  dvdsmulcr  12511  dvdsdivcl  12540  oddnn02np1  12570  ndvdsadd  12621  bitsinv1lem  12651  zeqzmulgcd  12670  bezoutlemmain  12698  dfgcd2  12714  gcdmultiple  12720  coprmdvds  12793  divgcdodd  12844  isprm6  12848  prmdvdsexpr  12851  cncongrprm  12858  phiprmpw  12923  modprm0  12956  pythagtriplem4  12970  pcz  13034  difsqpwdvds  13040  pcadd  13042  1arith  13069  ballotfilemfc0  13153  ballotfilemfcc  13154  isgrpid2  13770  ghmghmrn  13997  ghmf1  14007  kerf1ghm  14008  imasabl  14070  ringinvnz1ne0  14210  subrngringnsg  14367  domnmuln0  14436  rnglidlmcl  14645  znf1o  14816  znidom  14822  lmss  15128  cnplimcim  15549  dvcn  15582  fsumdvdsmul  15876  gausslemma2dlem1a  15948  lgseisenlem2  15961  lgsquad2  15973  2lgslem1b  15979  2sqlem6  16010  upgrpredgv  16158  upgredgpr  16161  uhgr0v0e  16246  subgrprop  16271  wlkpropg  16336  upgrwlkcompim  16374  uspgr2wlkeq  16377  wlklenvclwlk  16385  wlkres  16391  clwwlk1loop  16411  umgrclwwlkge2  16414  clwwlkn1loopb  16432  clwwlknonex2lem2  16450  ch2var  16556  bj-rspgt  16575  bj-charfundcALT  16596  bj-nntrans  16738  bj-nnelirr  16740  bj-omtrans  16743  setindft  16752  bj-inf2vnlem3  16759  bj-inf2vnlem4  16760  bj-findis  16766  pw1nct  16794