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  674  mtbiri  676  orbi2d  791  pm5.15dc  1400  exlimd2  1609  exintr  1648  19.9d  1675  19.23t  1691  chvarfv  1714  dral1  1744  spimt  1750  cbvalv1  1765  cbvalh  1767  chvar  1771  exdistrfor  1814  sbequi  1853  spv  1874  cbvexvw  1935  eqrdav  2195  cleqh  2296  ceqsalg  2791  vtoclf  2817  vtocl2  2819  vtocl3  2820  spcdv  2849  rspcdv  2871  elabgt  2905  sbcn1  3037  sbcim1  3038  sbcbi1  3039  sbeqalb  3046  sbcel21v  3054  eqrd  3202  exmidsssn  4236  exmidsssnc  4237  copsexg  4278  euotd  4288  rexxfrd  4499  relop  4817  elres  4983  rnxpid  5105  relcnvtr  5190  iotaval  5231  mpteqb  5655  elfvmptrab  5660  chfnrn  5676  elpreima  5684  ffnfv  5723  f1elima  5823  f1eqcocnv  5841  fliftfun  5846  isoresbr  5859  isotr  5866  ovmpodv2  6060  smoiso  6369  nnaordi  6575  nnaword  6578  nnawordi  6582  xpider  6674  iinerm  6675  mptelixpg  6802  dom2lem  6840  nneneq  6927  exmidpw  6978  infidc  7009  f1dmvrnfibi  7019  ismkvnex  7230  pr2nelem  7270  exmidfodomrlemeldju  7278  exmidfodomrlemreseldju  7279  netap  7337  2omotaplemap  7340  addcanpig  7418  mulcanpig  7419  enqer  7442  ltexnqi  7493  prarloclemlo  7578  genpcdl  7603  genpcuu  7604  appdivnq  7647  ltprordil  7673  1idprl  7674  1idpru  7675  ltexprlemm  7684  ltexprlemopu  7687  ltexprlemru  7696  cauappcvgprlemladdru  7740  cauappcvgprlemladdrl  7741  caucvgprprlemopu  7783  caucvgsrlemoffcau  7882  caucvgsrlemoffres  7884  ltrenn  7939  axpre-ltadd  7970  addn0nid  8417  apne  8667  aptap  8694  prodgt02  8897  prodge02  8899  mulgt1  8907  divgt0  8916  divge0  8917  cju  9005  nnsub  9046  nominpos  9246  zltnle  9389  nn0n0n1ge2  9413  zdcle  9419  btwnnz  9437  uzm1  9649  supinfneg  9686  infsupneg  9687  ublbneg  9704  cnref1o  9742  ltsubrp  9782  ltaddrp  9783  xnn0dcle  9894  npnflt  9907  nmnfgt  9910  ge0nemnf  9916  xltnegi  9927  xnn0xadd0  9959  iccsupr  10058  icoshft  10082  iccshftri  10087  iccshftli  10089  iccdili  10091  icccntri  10093  fzdcel  10132  fznlem  10133  fzen  10135  fzofzim  10281  eluzgtdifelfzo  10290  elfzonelfzo  10323  qltnle  10350  addmodlteq  10507  qsqeqor  10759  apexp1  10827  fihashf1rn  10897  cjre  11064  caucvgre  11163  icodiamlt  11362  zsumdc  11566  zproddc  11761  reeff1  11882  dvdsmod0  11975  dvds2lem  11985  muldvds1  11998  dvdscmulr  12002  dvdsmulcr  12003  dvdsdivcl  12032  oddnn02np1  12062  ndvdsadd  12113  bitsinv1lem  12143  zeqzmulgcd  12162  bezoutlemmain  12190  dfgcd2  12206  gcdmultiple  12212  coprmdvds  12285  divgcdodd  12336  isprm6  12340  prmdvdsexpr  12343  cncongrprm  12350  phiprmpw  12415  modprm0  12448  pythagtriplem4  12462  pcz  12526  difsqpwdvds  12532  pcadd  12534  1arith  12561  isgrpid2  13242  ghmghmrn  13469  ghmf1  13479  kerf1ghm  13480  imasabl  13542  ringinvnz1ne0  13681  subrngringnsg  13837  domnmuln0  13905  rnglidlmcl  14112  znf1o  14283  znidom  14289  lmss  14566  cnplimcim  14987  dvcn  15020  fsumdvdsmul  15311  gausslemma2dlem1a  15383  lgseisenlem2  15396  lgsquad2  15408  2lgslem1b  15414  2sqlem6  15445  ch2var  15497  bj-rspgt  15516  bj-charfundcALT  15539  bj-nntrans  15681  bj-nnelirr  15683  bj-omtrans  15686  setindft  15695  bj-inf2vnlem3  15702  bj-inf2vnlem4  15703  bj-findis  15709  pw1nct  15734