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  680  mtbiri  682  orbi2d  798  pm5.15dc  1434  exlimd2  1644  exintr  1683  19.9d  1709  19.23t  1725  chvarfv  1748  dral1  1779  spimt  1785  cbvalv1  1800  cbvalh  1802  chvar  1806  exdistrfor  1849  sbequi  1888  spv  1909  cbvexvw  1972  eqrdav  2233  cleqh  2334  ceqsalg  2844  vtoclf  2870  vtocl2  2872  vtocl3  2873  spcdv  2904  rspcdv  2926  elabgt  2961  sbcn1  3093  sbcim1  3094  sbcbi1  3095  sbeqalb  3102  sbcel21v  3110  eqrd  3260  ifeqeqxdc  3673  rabsnifsb  3762  exmidsssn  4320  exmidsssnc  4321  copsexg  4365  euotd  4376  rexxfrd  4589  relop  4910  reldmm  4980  elres  5079  rnxpid  5202  relcnvtr  5287  iotaval  5329  mpteqb  5773  elfvmptrab  5778  chfnrn  5794  elpreima  5802  ffnfv  5840  f1elima  5952  f1eqcocnv  5970  fliftfun  5975  isoresbr  5988  isotr  5995  ovmpodv2  6195  ressuppss  6467  funsssuppss  6471  smoiso  6546  nnaordi  6754  nnaword  6757  nnawordi  6761  xpider  6853  iinerm  6854  mptelixpg  6982  dom2lem  7024  nneneq  7124  exmidpw  7181  infidc  7214  f1dmvrnfibi  7224  fsuppimp  7258  ismkvnex  7459  pr2nelem  7501  exmidfodomrlemeldju  7515  exmidfodomrlemreseldju  7516  netap  7584  2omotaplemap  7587  addcanpig  7665  mulcanpig  7666  enqer  7689  ltexnqi  7740  prarloclemlo  7825  genpcdl  7850  genpcuu  7851  appdivnq  7894  ltprordil  7920  1idprl  7921  1idpru  7922  ltexprlemm  7931  ltexprlemopu  7934  ltexprlemru  7943  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  caucvgprprlemopu  8030  caucvgsrlemoffcau  8129  caucvgsrlemoffres  8131  ltrenn  8186  axpre-ltadd  8217  addn0nid  8663  apne  8914  aptap  8941  prodgt02  9144  prodge02  9146  mulgt1  9154  divgt0  9163  divge0  9164  cju  9252  nnsub  9293  nominpos  9493  zltnle  9640  nn0n0n1ge2  9665  zdcle  9671  btwnnz  9690  uzm1  9903  supinfneg  9945  infsupneg  9946  ublbneg  9963  cnref1o  10001  ltsubrp  10041  ltaddrp  10042  xnn0dcle  10154  npnflt  10167  nmnfgt  10170  ge0nemnf  10176  xltnegi  10187  xnn0xadd0  10219  iccsupr  10318  icoshft  10342  iccshftri  10347  iccshftli  10349  iccdili  10351  icccntri  10353  fzdcel  10394  fznlem  10395  fzen  10397  fzofzim  10549  eluzgtdifelfzo  10564  elfzonelfzo  10597  qltnle  10627  addmodlteq  10784  qsqeqor  11036  apexp1  11105  fihashf1rn  11176  lswlgt0cl  11302  ccatalpha  11326  pfxfv  11401  pfxsuff1eqwrdeq  11416  ccatopth2  11434  swrdccat  11452  swrdccat3blem  11456  reuccatpfxs1lem  11463  cjre  11592  caucvgre  11691  icodiamlt  11890  zsumdc  12095  zproddc  12290  reeff1  12411  dvdsmod0  12504  dvds2lem  12514  muldvds1  12527  dvdscmulr  12531  dvdsmulcr  12532  dvdsdivcl  12561  oddnn02np1  12591  ndvdsadd  12642  bitsinv1lem  12672  zeqzmulgcd  12691  bezoutlemmain  12719  dfgcd2  12735  gcdmultiple  12741  coprmdvds  12814  divgcdodd  12865  isprm6  12869  prmdvdsexpr  12872  cncongrprm  12879  phiprmpw  12944  modprm0  12977  pythagtriplem4  12991  pcz  13055  difsqpwdvds  13061  pcadd  13063  1arith  13090  ballotfilemfc0  13176  ballotfilemfcc  13177  isgrpid2  13795  ghmghmrn  14016  ghmf1  14026  kerf1ghm  14027  imasabl  14089  rng1zrlem  14198  ringinvnz1ne0  14292  subrngringnsg  14451  domnmuln0  14520  rnglidlmcl  14754  znf1o  14925  znidom  14931  lmss  15237  cnplimcim  15658  dvcn  15691  fsumdvdsmul  15985  gausslemma2dlem1a  16057  lgseisenlem2  16070  lgsquad2  16082  2lgslem1b  16088  2sqlem6  16119  upgrpredgv  16267  upgredgpr  16270  uhgr0v0e  16355  subgrprop  16380  wlkpropg  16445  upgrwlkcompim  16483  uspgr2wlkeq  16486  wlklenvclwlk  16494  wlkres  16500  clwwlk1loop  16520  umgrclwwlkge2  16523  clwwlkn1loopb  16541  clwwlknonex2lem2  16559  ch2var  16665  bj-rspgt  16684  bj-charfundcALT  16705  bj-nntrans  16847  bj-nnelirr  16849  bj-omtrans  16852  setindft  16861  bj-inf2vnlem3  16868  bj-inf2vnlem4  16869  bj-findis  16875  pw1nct  16903