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  684  mtbiri  686  orbi2d  802  pm5.15dc  1438  exlimd2  1648  exintr  1687  19.9d  1713  19.23t  1729  chvarfv  1752  dral1  1783  spimt  1789  cbvalv1  1804  cbvalh  1806  chvar  1810  exdistrfor  1853  sbequi  1892  spv  1913  cbvexvw  1976  eqrdav  2237  cleqh  2338  ceqsalg  2850  vtoclf  2876  vtocl2  2878  vtocl3  2879  spcdv  2910  rspcdv  2932  elabgt  2967  sbcn1  3099  sbcim1  3100  sbcbi1  3101  sbeqalb  3108  sbcel21v  3116  eqrd  3266  ifeqeqxdc  3684  rabsnifsb  3773  exmidsssn  4334  exmidsssnc  4335  copsexg  4379  euotd  4390  rexxfrd  4604  relop  4925  reldmm  4995  elres  5094  rnxpid  5217  relcnvtr  5302  iotaval  5344  mpteqb  5790  elfvmptrab  5795  chfnrn  5811  elpreima  5819  ffnfv  5857  f1elima  5969  f1eqcocnv  5987  fliftfun  5992  isoresbr  6005  isotr  6012  ovmpodv2  6212  ressuppss  6484  funsssuppss  6488  smoiso  6563  nnaordi  6771  nnaword  6774  nnawordi  6778  xpider  6870  iinerm  6871  mptelixpg  7006  dom2lem  7048  nneneq  7148  exmidpw  7205  infidc  7238  f1dmvrnfibi  7248  fsuppimp  7282  ismkvnex  7485  pr2nelem  7527  exmidfodomrlemeldju  7541  exmidfodomrlemreseldju  7542  netap  7610  2omotaplemap  7613  addcanpig  7691  mulcanpig  7692  enqer  7715  ltexnqi  7766  prarloclemlo  7851  genpcdl  7876  genpcuu  7877  appdivnq  7920  ltprordil  7946  1idprl  7947  1idpru  7948  ltexprlemm  7957  ltexprlemopu  7960  ltexprlemru  7969  cauappcvgprlemladdru  8013  cauappcvgprlemladdrl  8014  caucvgprprlemopu  8056  caucvgsrlemoffcau  8155  caucvgsrlemoffres  8157  ltrenn  8212  axpre-ltadd  8243  addn0nid  8690  apne  8941  aptap  8968  prodgt02  9173  prodge02  9175  mulgt1  9183  divgt0  9192  divge0  9193  cju  9281  nnsub  9322  nominpos  9522  zltnle  9669  nn0n0n1ge2  9694  zdcle  9700  btwnnz  9719  uzm1  9932  supinfneg  9974  infsupneg  9975  ublbneg  9992  cnref1o  10030  ltsubrp  10070  ltaddrp  10071  xnn0dcle  10183  npnflt  10196  nmnfgt  10199  ge0nemnf  10205  xltnegi  10216  xnn0xadd0  10248  iccsupr  10347  icoshft  10371  iccshftri  10376  iccshftli  10378  iccdili  10380  icccntri  10382  fzdcel  10423  fznlem  10424  fzen  10426  fzofzim  10578  eluzgtdifelfzo  10593  elfzonelfzo  10626  qltnle  10656  addmodlteq  10813  qsqeqor  11065  apexp1  11134  fihashf1rn  11205  lswlgt0cl  11335  ccatalpha  11359  pfxfv  11434  pfxsuff1eqwrdeq  11449  ccatopth2  11467  swrdccat  11485  swrdccat3blem  11489  reuccatpfxs1lem  11496  cjre  11625  caucvgre  11725  icodiamlt  11924  zsumdc  12129  zproddc  12324  reeff1  12445  dvdsmod0  12538  dvds2lem  12548  muldvds1  12561  dvdscmulr  12565  dvdsmulcr  12566  dvdsdivcl  12595  oddnn02np1  12625  ndvdsadd  12676  bitsinv1lem  12706  zeqzmulgcd  12725  bezoutlemmain  12753  dfgcd2  12769  gcdmultiple  12775  coprmdvds  12848  divgcdodd  12899  isprm6  12903  prmdvdsexpr  12906  cncongrprm  12913  phiprmpw  12978  modprm0  13011  pythagtriplem4  13025  pcz  13089  difsqpwdvds  13095  pcadd  13097  1arith  13124  ballotfilemfc0  13210  ballotfilemfcc  13211  isgrpid2  13822  ghmghmrn  14043  ghmf1  14053  kerf1ghm  14054  imasabl  14117  rng1zrlem  14233  ringinvnz1ne0  14327  subrngringnsg  14486  domnmuln0  14555  rnglidlmcl  14789  znf1o  14958  znidom  14964  lmss  15270  cnplimcim  15691  dvcn  15724  fsumdvdsmul  16019  gausslemma2dlem1a  16091  lgseisenlem2  16104  lgsquad2  16116  2lgslem1b  16122  2sqlem6  16153  upgrpredgv  16301  upgredgpr  16304  uhgr0v0e  16389  subgrprop  16414  wlkpropg  16479  upgrwlkcompim  16517  uspgr2wlkeq  16520  wlklenvclwlk  16528  wlkres  16534  clwwlk1loop  16554  umgrclwwlkge2  16557  clwwlkn1loopb  16575  clwwlknonex2lem2  16593  ch2var  16709  bj-rspgt  16728  bj-charfundcALT  16749  bj-nntrans  16891  bj-nnelirr  16893  bj-omtrans  16896  setindft  16905  bj-inf2vnlem3  16912  bj-inf2vnlem4  16913  bj-findis  16919  pw1nct  16947