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  7078  infidc  7109  f1dmvrnfibi  7119  ismkvnex  7330  pr2nelem  7372  exmidfodomrlemeldju  7385  exmidfodomrlemreseldju  7386  netap  7448  2omotaplemap  7451  addcanpig  7529  mulcanpig  7530  enqer  7553  ltexnqi  7604  prarloclemlo  7689  genpcdl  7714  genpcuu  7715  appdivnq  7758  ltprordil  7784  1idprl  7785  1idpru  7786  ltexprlemm  7795  ltexprlemopu  7798  ltexprlemru  7807  cauappcvgprlemladdru  7851  cauappcvgprlemladdrl  7852  caucvgprprlemopu  7894  caucvgsrlemoffcau  7993  caucvgsrlemoffres  7995  ltrenn  8050  axpre-ltadd  8081  addn0nid  8528  apne  8778  aptap  8805  prodgt02  9008  prodge02  9010  mulgt1  9018  divgt0  9027  divge0  9028  cju  9116  nnsub  9157  nominpos  9357  zltnle  9500  nn0n0n1ge2  9525  zdcle  9531  btwnnz  9549  uzm1  9761  supinfneg  9798  infsupneg  9799  ublbneg  9816  cnref1o  9854  ltsubrp  9894  ltaddrp  9895  xnn0dcle  10006  npnflt  10019  nmnfgt  10022  ge0nemnf  10028  xltnegi  10039  xnn0xadd0  10071  iccsupr  10170  icoshft  10194  iccshftri  10199  iccshftli  10201  iccdili  10203  icccntri  10205  fzdcel  10244  fznlem  10245  fzen  10247  fzofzim  10396  eluzgtdifelfzo  10411  elfzonelfzo  10444  qltnle  10471  addmodlteq  10628  qsqeqor  10880  apexp1  10948  fihashf1rn  11018  lswlgt0cl  11132  pfxfv  11224  pfxsuff1eqwrdeq  11239  ccatopth2  11257  swrdccat  11275  swrdccat3blem  11279  reuccatpfxs1lem  11286  cjre  11401  caucvgre  11500  icodiamlt  11699  zsumdc  11903  zproddc  12098  reeff1  12219  dvdsmod0  12312  dvds2lem  12322  muldvds1  12335  dvdscmulr  12339  dvdsmulcr  12340  dvdsdivcl  12369  oddnn02np1  12399  ndvdsadd  12450  bitsinv1lem  12480  zeqzmulgcd  12499  bezoutlemmain  12527  dfgcd2  12543  gcdmultiple  12549  coprmdvds  12622  divgcdodd  12673  isprm6  12677  prmdvdsexpr  12680  cncongrprm  12687  phiprmpw  12752  modprm0  12785  pythagtriplem4  12799  pcz  12863  difsqpwdvds  12869  pcadd  12871  1arith  12898  isgrpid2  13581  ghmghmrn  13808  ghmf1  13818  kerf1ghm  13819  imasabl  13881  ringinvnz1ne0  14020  subrngringnsg  14177  domnmuln0  14245  rnglidlmcl  14452  znf1o  14623  znidom  14629  lmss  14928  cnplimcim  15349  dvcn  15382  fsumdvdsmul  15673  gausslemma2dlem1a  15745  lgseisenlem2  15758  lgsquad2  15770  2lgslem1b  15776  2sqlem6  15807  upgrpredgv  15952  upgredgpr  15955  wlkpropg  16045  upgrwlkcompim  16083  uspgr2wlkeq  16086  wlklenvclwlk  16094  wlkres  16098  ch2var  16155  bj-rspgt  16174  bj-charfundcALT  16196  bj-nntrans  16338  bj-nnelirr  16340  bj-omtrans  16343  setindft  16352  bj-inf2vnlem3  16359  bj-inf2vnlem4  16360  bj-findis  16366  pw1nct  16395