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  675  mtbiri  677  orbi2d  792  pm5.15dc  1409  exlimd2  1619  exintr  1658  19.9d  1685  19.23t  1701  chvarfv  1724  dral1  1754  spimt  1760  cbvalv1  1775  cbvalh  1777  chvar  1781  exdistrfor  1824  sbequi  1863  spv  1884  cbvexvw  1945  eqrdav  2206  cleqh  2307  ceqsalg  2805  vtoclf  2831  vtocl2  2833  vtocl3  2834  spcdv  2865  rspcdv  2887  elabgt  2921  sbcn1  3053  sbcim1  3054  sbcbi1  3055  sbeqalb  3062  sbcel21v  3070  eqrd  3219  exmidsssn  4262  exmidsssnc  4263  copsexg  4306  euotd  4317  rexxfrd  4528  relop  4846  elres  5014  rnxpid  5136  relcnvtr  5221  iotaval  5262  mpteqb  5693  elfvmptrab  5698  chfnrn  5714  elpreima  5722  ffnfv  5761  f1elima  5865  f1eqcocnv  5883  fliftfun  5888  isoresbr  5901  isotr  5908  ovmpodv2  6102  smoiso  6411  nnaordi  6617  nnaword  6620  nnawordi  6624  xpider  6716  iinerm  6717  mptelixpg  6844  dom2lem  6886  nneneq  6979  exmidpw  7031  infidc  7062  f1dmvrnfibi  7072  ismkvnex  7283  pr2nelem  7325  exmidfodomrlemeldju  7338  exmidfodomrlemreseldju  7339  netap  7401  2omotaplemap  7404  addcanpig  7482  mulcanpig  7483  enqer  7506  ltexnqi  7557  prarloclemlo  7642  genpcdl  7667  genpcuu  7668  appdivnq  7711  ltprordil  7737  1idprl  7738  1idpru  7739  ltexprlemm  7748  ltexprlemopu  7751  ltexprlemru  7760  cauappcvgprlemladdru  7804  cauappcvgprlemladdrl  7805  caucvgprprlemopu  7847  caucvgsrlemoffcau  7946  caucvgsrlemoffres  7948  ltrenn  8003  axpre-ltadd  8034  addn0nid  8481  apne  8731  aptap  8758  prodgt02  8961  prodge02  8963  mulgt1  8971  divgt0  8980  divge0  8981  cju  9069  nnsub  9110  nominpos  9310  zltnle  9453  nn0n0n1ge2  9478  zdcle  9484  btwnnz  9502  uzm1  9714  supinfneg  9751  infsupneg  9752  ublbneg  9769  cnref1o  9807  ltsubrp  9847  ltaddrp  9848  xnn0dcle  9959  npnflt  9972  nmnfgt  9975  ge0nemnf  9981  xltnegi  9992  xnn0xadd0  10024  iccsupr  10123  icoshft  10147  iccshftri  10152  iccshftli  10154  iccdili  10156  icccntri  10158  fzdcel  10197  fznlem  10198  fzen  10200  fzofzim  10349  eluzgtdifelfzo  10363  elfzonelfzo  10396  qltnle  10423  addmodlteq  10580  qsqeqor  10832  apexp1  10900  fihashf1rn  10970  lswlgt0cl  11083  pfxfv  11175  pfxsuff1eqwrdeq  11190  ccatopth2  11208  swrdccat  11226  swrdccat3blem  11230  reuccatpfxs1lem  11237  cjre  11308  caucvgre  11407  icodiamlt  11606  zsumdc  11810  zproddc  12005  reeff1  12126  dvdsmod0  12219  dvds2lem  12229  muldvds1  12242  dvdscmulr  12246  dvdsmulcr  12247  dvdsdivcl  12276  oddnn02np1  12306  ndvdsadd  12357  bitsinv1lem  12387  zeqzmulgcd  12406  bezoutlemmain  12434  dfgcd2  12450  gcdmultiple  12456  coprmdvds  12529  divgcdodd  12580  isprm6  12584  prmdvdsexpr  12587  cncongrprm  12594  phiprmpw  12659  modprm0  12692  pythagtriplem4  12706  pcz  12770  difsqpwdvds  12776  pcadd  12778  1arith  12805  isgrpid2  13487  ghmghmrn  13714  ghmf1  13724  kerf1ghm  13725  imasabl  13787  ringinvnz1ne0  13926  subrngringnsg  14082  domnmuln0  14150  rnglidlmcl  14357  znf1o  14528  znidom  14534  lmss  14833  cnplimcim  15254  dvcn  15287  fsumdvdsmul  15578  gausslemma2dlem1a  15650  lgseisenlem2  15663  lgsquad2  15675  2lgslem1b  15681  2sqlem6  15712  upgrpredgv  15850  upgredgpr  15853  ch2var  15903  bj-rspgt  15922  bj-charfundcALT  15944  bj-nntrans  16086  bj-nnelirr  16088  bj-omtrans  16091  setindft  16100  bj-inf2vnlem3  16107  bj-inf2vnlem4  16108  bj-findis  16114  pw1nct  16142