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  679  mtbiri  681  orbi2d  797  pm5.15dc  1433  exlimd2  1643  exintr  1682  19.9d  1709  19.23t  1725  chvarfv  1748  dral1  1778  spimt  1784  cbvalv1  1799  cbvalh  1801  chvar  1805  exdistrfor  1848  sbequi  1887  spv  1908  cbvexvw  1969  eqrdav  2230  cleqh  2331  ceqsalg  2831  vtoclf  2857  vtocl2  2859  vtocl3  2860  spcdv  2891  rspcdv  2913  elabgt  2947  sbcn1  3079  sbcim1  3080  sbcbi1  3081  sbeqalb  3088  sbcel21v  3096  eqrd  3245  rabsnifsb  3737  exmidsssn  4292  exmidsssnc  4293  copsexg  4336  euotd  4347  rexxfrd  4560  relop  4880  reldmm  4950  elres  5049  rnxpid  5171  relcnvtr  5256  iotaval  5298  mpteqb  5737  elfvmptrab  5742  chfnrn  5758  elpreima  5766  ffnfv  5805  f1elima  5914  f1eqcocnv  5932  fliftfun  5937  isoresbr  5950  isotr  5957  ovmpodv2  6155  smoiso  6468  nnaordi  6676  nnaword  6679  nnawordi  6683  xpider  6775  iinerm  6776  mptelixpg  6903  dom2lem  6945  nneneq  7043  exmidpw  7100  infidc  7133  f1dmvrnfibi  7143  ismkvnex  7354  pr2nelem  7396  exmidfodomrlemeldju  7410  exmidfodomrlemreseldju  7411  netap  7473  2omotaplemap  7476  addcanpig  7554  mulcanpig  7555  enqer  7578  ltexnqi  7629  prarloclemlo  7714  genpcdl  7739  genpcuu  7740  appdivnq  7783  ltprordil  7809  1idprl  7810  1idpru  7811  ltexprlemm  7820  ltexprlemopu  7823  ltexprlemru  7832  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  caucvgprprlemopu  7919  caucvgsrlemoffcau  8018  caucvgsrlemoffres  8020  ltrenn  8075  axpre-ltadd  8106  addn0nid  8553  apne  8803  aptap  8830  prodgt02  9033  prodge02  9035  mulgt1  9043  divgt0  9052  divge0  9053  cju  9141  nnsub  9182  nominpos  9382  zltnle  9525  nn0n0n1ge2  9550  zdcle  9556  btwnnz  9574  uzm1  9787  supinfneg  9829  infsupneg  9830  ublbneg  9847  cnref1o  9885  ltsubrp  9925  ltaddrp  9926  xnn0dcle  10037  npnflt  10050  nmnfgt  10053  ge0nemnf  10059  xltnegi  10070  xnn0xadd0  10102  iccsupr  10201  icoshft  10225  iccshftri  10230  iccshftli  10232  iccdili  10234  icccntri  10236  fzdcel  10275  fznlem  10276  fzen  10278  fzofzim  10428  eluzgtdifelfzo  10443  elfzonelfzo  10476  qltnle  10504  addmodlteq  10661  qsqeqor  10913  apexp1  10981  fihashf1rn  11051  lswlgt0cl  11170  ccatalpha  11194  pfxfv  11269  pfxsuff1eqwrdeq  11284  ccatopth2  11302  swrdccat  11320  swrdccat3blem  11324  reuccatpfxs1lem  11331  cjre  11460  caucvgre  11559  icodiamlt  11758  zsumdc  11963  zproddc  12158  reeff1  12279  dvdsmod0  12372  dvds2lem  12382  muldvds1  12395  dvdscmulr  12399  dvdsmulcr  12400  dvdsdivcl  12429  oddnn02np1  12459  ndvdsadd  12510  bitsinv1lem  12540  zeqzmulgcd  12559  bezoutlemmain  12587  dfgcd2  12603  gcdmultiple  12609  coprmdvds  12682  divgcdodd  12733  isprm6  12737  prmdvdsexpr  12740  cncongrprm  12747  phiprmpw  12812  modprm0  12845  pythagtriplem4  12859  pcz  12923  difsqpwdvds  12929  pcadd  12931  1arith  12958  isgrpid2  13641  ghmghmrn  13868  ghmf1  13878  kerf1ghm  13879  imasabl  13941  ringinvnz1ne0  14081  subrngringnsg  14238  domnmuln0  14306  rnglidlmcl  14513  znf1o  14684  znidom  14690  lmss  14989  cnplimcim  15410  dvcn  15443  fsumdvdsmul  15734  gausslemma2dlem1a  15806  lgseisenlem2  15819  lgsquad2  15831  2lgslem1b  15837  2sqlem6  15868  upgrpredgv  16016  upgredgpr  16019  uhgr0v0e  16104  subgrprop  16129  wlkpropg  16194  upgrwlkcompim  16232  uspgr2wlkeq  16235  wlklenvclwlk  16243  wlkres  16249  clwwlk1loop  16269  umgrclwwlkge2  16272  clwwlkn1loopb  16290  clwwlknonex2lem2  16308  ch2var  16414  bj-rspgt  16433  bj-charfundcALT  16455  bj-nntrans  16597  bj-nnelirr  16599  bj-omtrans  16602  setindft  16611  bj-inf2vnlem3  16618  bj-inf2vnlem4  16619  bj-findis  16625  pw1nct  16655