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  1778  spimt  1784  cbvalv1  1799  cbvalh  1801  chvar  1805  exdistrfor  1848  sbequi  1887  spv  1908  cbvexvw  1969  eqrdav  2230  cleqh  2331  ceqsalg  2832  vtoclf  2858  vtocl2  2860  vtocl3  2861  spcdv  2892  rspcdv  2914  elabgt  2948  sbcn1  3080  sbcim1  3081  sbcbi1  3082  sbeqalb  3089  sbcel21v  3097  eqrd  3246  rabsnifsb  3741  exmidsssn  4298  exmidsssnc  4299  copsexg  4342  euotd  4353  rexxfrd  4566  relop  4886  reldmm  4956  elres  5055  rnxpid  5178  relcnvtr  5263  iotaval  5305  mpteqb  5746  elfvmptrab  5751  chfnrn  5767  elpreima  5775  ffnfv  5813  f1elima  5924  f1eqcocnv  5942  fliftfun  5947  isoresbr  5960  isotr  5967  ovmpodv2  6165  ressuppss  6432  funsssuppss  6436  smoiso  6511  nnaordi  6719  nnaword  6722  nnawordi  6726  xpider  6818  iinerm  6819  mptelixpg  6946  dom2lem  6988  nneneq  7086  exmidpw  7143  infidc  7176  f1dmvrnfibi  7186  fsuppimp  7217  ismkvnex  7414  pr2nelem  7456  exmidfodomrlemeldju  7470  exmidfodomrlemreseldju  7471  netap  7533  2omotaplemap  7536  addcanpig  7614  mulcanpig  7615  enqer  7638  ltexnqi  7689  prarloclemlo  7774  genpcdl  7799  genpcuu  7800  appdivnq  7843  ltprordil  7869  1idprl  7870  1idpru  7871  ltexprlemm  7880  ltexprlemopu  7883  ltexprlemru  7892  cauappcvgprlemladdru  7936  cauappcvgprlemladdrl  7937  caucvgprprlemopu  7979  caucvgsrlemoffcau  8078  caucvgsrlemoffres  8080  ltrenn  8135  axpre-ltadd  8166  addn0nid  8612  apne  8862  aptap  8889  prodgt02  9092  prodge02  9094  mulgt1  9102  divgt0  9111  divge0  9112  cju  9200  nnsub  9241  nominpos  9441  zltnle  9586  nn0n0n1ge2  9611  zdcle  9617  btwnnz  9635  uzm1  9848  supinfneg  9890  infsupneg  9891  ublbneg  9908  cnref1o  9946  ltsubrp  9986  ltaddrp  9987  xnn0dcle  10098  npnflt  10111  nmnfgt  10114  ge0nemnf  10120  xltnegi  10131  xnn0xadd0  10163  iccsupr  10262  icoshft  10286  iccshftri  10291  iccshftli  10293  iccdili  10295  icccntri  10297  fzdcel  10337  fznlem  10338  fzen  10340  fzofzim  10490  eluzgtdifelfzo  10505  elfzonelfzo  10538  qltnle  10566  addmodlteq  10723  qsqeqor  10975  apexp1  11043  fihashf1rn  11113  lswlgt0cl  11232  ccatalpha  11256  pfxfv  11331  pfxsuff1eqwrdeq  11346  ccatopth2  11364  swrdccat  11382  swrdccat3blem  11386  reuccatpfxs1lem  11393  cjre  11522  caucvgre  11621  icodiamlt  11820  zsumdc  12025  zproddc  12220  reeff1  12341  dvdsmod0  12434  dvds2lem  12444  muldvds1  12457  dvdscmulr  12461  dvdsmulcr  12462  dvdsdivcl  12491  oddnn02np1  12521  ndvdsadd  12572  bitsinv1lem  12602  zeqzmulgcd  12621  bezoutlemmain  12649  dfgcd2  12665  gcdmultiple  12671  coprmdvds  12744  divgcdodd  12795  isprm6  12799  prmdvdsexpr  12802  cncongrprm  12809  phiprmpw  12874  modprm0  12907  pythagtriplem4  12921  pcz  12985  difsqpwdvds  12991  pcadd  12993  1arith  13020  isgrpid2  13703  ghmghmrn  13930  ghmf1  13940  kerf1ghm  13941  imasabl  14003  ringinvnz1ne0  14143  subrngringnsg  14300  domnmuln0  14369  rnglidlmcl  14576  znf1o  14747  znidom  14753  lmss  15057  cnplimcim  15478  dvcn  15511  fsumdvdsmul  15805  gausslemma2dlem1a  15877  lgseisenlem2  15890  lgsquad2  15902  2lgslem1b  15908  2sqlem6  15939  upgrpredgv  16087  upgredgpr  16090  uhgr0v0e  16175  subgrprop  16200  wlkpropg  16265  upgrwlkcompim  16303  uspgr2wlkeq  16306  wlklenvclwlk  16314  wlkres  16320  clwwlk1loop  16340  umgrclwwlkge2  16343  clwwlkn1loopb  16361  clwwlknonex2lem2  16379  ch2var  16485  bj-rspgt  16504  bj-charfundcALT  16525  bj-nntrans  16667  bj-nnelirr  16669  bj-omtrans  16672  setindft  16681  bj-inf2vnlem3  16688  bj-inf2vnlem4  16689  bj-findis  16695  pw1nct  16725