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  677  mtbiri  679  orbi2d  795  pm5.15dc  1431  exlimd2  1641  exintr  1680  19.9d  1707  19.23t  1723  chvarfv  1746  dral1  1776  spimt  1782  cbvalv1  1797  cbvalh  1799  chvar  1803  exdistrfor  1846  sbequi  1885  spv  1906  cbvexvw  1967  eqrdav  2228  cleqh  2329  ceqsalg  2828  vtoclf  2854  vtocl2  2856  vtocl3  2857  spcdv  2888  rspcdv  2910  elabgt  2944  sbcn1  3076  sbcim1  3077  sbcbi1  3078  sbeqalb  3085  sbcel21v  3093  eqrd  3242  exmidsssn  4286  exmidsssnc  4287  copsexg  4330  euotd  4341  rexxfrd  4554  relop  4872  reldmm  4942  elres  5041  rnxpid  5163  relcnvtr  5248  iotaval  5290  mpteqb  5727  elfvmptrab  5732  chfnrn  5748  elpreima  5756  ffnfv  5795  f1elima  5903  f1eqcocnv  5921  fliftfun  5926  isoresbr  5939  isotr  5946  ovmpodv2  6144  smoiso  6454  nnaordi  6662  nnaword  6665  nnawordi  6669  xpider  6761  iinerm  6762  mptelixpg  6889  dom2lem  6931  nneneq  7026  exmidpw  7081  infidc  7112  f1dmvrnfibi  7122  ismkvnex  7333  pr2nelem  7375  exmidfodomrlemeldju  7388  exmidfodomrlemreseldju  7389  netap  7451  2omotaplemap  7454  addcanpig  7532  mulcanpig  7533  enqer  7556  ltexnqi  7607  prarloclemlo  7692  genpcdl  7717  genpcuu  7718  appdivnq  7761  ltprordil  7787  1idprl  7788  1idpru  7789  ltexprlemm  7798  ltexprlemopu  7801  ltexprlemru  7810  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  caucvgprprlemopu  7897  caucvgsrlemoffcau  7996  caucvgsrlemoffres  7998  ltrenn  8053  axpre-ltadd  8084  addn0nid  8531  apne  8781  aptap  8808  prodgt02  9011  prodge02  9013  mulgt1  9021  divgt0  9030  divge0  9031  cju  9119  nnsub  9160  nominpos  9360  zltnle  9503  nn0n0n1ge2  9528  zdcle  9534  btwnnz  9552  uzm1  9765  supinfneg  9802  infsupneg  9803  ublbneg  9820  cnref1o  9858  ltsubrp  9898  ltaddrp  9899  xnn0dcle  10010  npnflt  10023  nmnfgt  10026  ge0nemnf  10032  xltnegi  10043  xnn0xadd0  10075  iccsupr  10174  icoshft  10198  iccshftri  10203  iccshftli  10205  iccdili  10207  icccntri  10209  fzdcel  10248  fznlem  10249  fzen  10251  fzofzim  10400  eluzgtdifelfzo  10415  elfzonelfzo  10448  qltnle  10475  addmodlteq  10632  qsqeqor  10884  apexp1  10952  fihashf1rn  11022  lswlgt0cl  11137  ccatalpha  11161  pfxfv  11232  pfxsuff1eqwrdeq  11247  ccatopth2  11265  swrdccat  11283  swrdccat3blem  11287  reuccatpfxs1lem  11294  cjre  11409  caucvgre  11508  icodiamlt  11707  zsumdc  11911  zproddc  12106  reeff1  12227  dvdsmod0  12320  dvds2lem  12330  muldvds1  12343  dvdscmulr  12347  dvdsmulcr  12348  dvdsdivcl  12377  oddnn02np1  12407  ndvdsadd  12458  bitsinv1lem  12488  zeqzmulgcd  12507  bezoutlemmain  12535  dfgcd2  12551  gcdmultiple  12557  coprmdvds  12630  divgcdodd  12681  isprm6  12685  prmdvdsexpr  12688  cncongrprm  12695  phiprmpw  12760  modprm0  12793  pythagtriplem4  12807  pcz  12871  difsqpwdvds  12877  pcadd  12879  1arith  12906  isgrpid2  13589  ghmghmrn  13816  ghmf1  13826  kerf1ghm  13827  imasabl  13889  ringinvnz1ne0  14028  subrngringnsg  14185  domnmuln0  14253  rnglidlmcl  14460  znf1o  14631  znidom  14637  lmss  14936  cnplimcim  15357  dvcn  15390  fsumdvdsmul  15681  gausslemma2dlem1a  15753  lgseisenlem2  15766  lgsquad2  15778  2lgslem1b  15784  2sqlem6  15815  upgrpredgv  15960  upgredgpr  15963  wlkpropg  16070  upgrwlkcompim  16108  uspgr2wlkeq  16111  wlklenvclwlk  16119  wlkres  16123  clwwlk1loop  16142  umgrclwwlkge2  16145  clwwlkn1loopb  16162  ch2var  16214  bj-rspgt  16233  bj-charfundcALT  16255  bj-nntrans  16397  bj-nnelirr  16399  bj-omtrans  16402  setindft  16411  bj-inf2vnlem3  16418  bj-inf2vnlem4  16419  bj-findis  16425  pw1nct  16456