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  674  mtbiri  676  orbi2d  791  pm5.15dc  1400  exlimd2  1606  exintr  1645  19.9d  1672  19.23t  1688  chvarfv  1711  dral1  1741  spimt  1747  cbvalv1  1762  cbvalh  1764  chvar  1768  exdistrfor  1811  sbequi  1850  spv  1871  cbvexvw  1932  eqrdav  2192  cleqh  2293  ceqsalg  2788  vtoclf  2814  vtocl2  2816  vtocl3  2817  spcdv  2846  rspcdv  2868  elabgt  2902  sbcn1  3034  sbcim1  3035  sbcbi1  3036  sbeqalb  3043  sbcel21v  3051  eqrd  3198  exmidsssn  4232  exmidsssnc  4233  copsexg  4274  euotd  4284  rexxfrd  4495  relop  4813  elres  4979  rnxpid  5101  relcnvtr  5186  iotaval  5227  mpteqb  5649  elfvmptrab  5654  chfnrn  5670  elpreima  5678  ffnfv  5717  f1elima  5817  f1eqcocnv  5835  fliftfun  5840  isoresbr  5853  isotr  5860  ovmpodv2  6053  smoiso  6357  nnaordi  6563  nnaword  6566  nnawordi  6570  xpider  6662  iinerm  6663  mptelixpg  6790  dom2lem  6828  nneneq  6915  exmidpw  6966  infidc  6995  f1dmvrnfibi  7005  ismkvnex  7216  pr2nelem  7253  exmidfodomrlemeldju  7261  exmidfodomrlemreseldju  7262  netap  7316  2omotaplemap  7319  addcanpig  7396  mulcanpig  7397  enqer  7420  ltexnqi  7471  prarloclemlo  7556  genpcdl  7581  genpcuu  7582  appdivnq  7625  ltprordil  7651  1idprl  7652  1idpru  7653  ltexprlemm  7662  ltexprlemopu  7665  ltexprlemru  7674  cauappcvgprlemladdru  7718  cauappcvgprlemladdrl  7719  caucvgprprlemopu  7761  caucvgsrlemoffcau  7860  caucvgsrlemoffres  7862  ltrenn  7917  axpre-ltadd  7948  addn0nid  8395  apne  8644  aptap  8671  prodgt02  8874  prodge02  8876  mulgt1  8884  divgt0  8893  divge0  8894  cju  8982  nnsub  9023  nominpos  9223  zltnle  9366  nn0n0n1ge2  9390  zdcle  9396  btwnnz  9414  uzm1  9626  supinfneg  9663  infsupneg  9664  ublbneg  9681  cnref1o  9719  ltsubrp  9759  ltaddrp  9760  xnn0dcle  9871  npnflt  9884  nmnfgt  9887  ge0nemnf  9893  xltnegi  9904  xnn0xadd0  9936  iccsupr  10035  icoshft  10059  iccshftri  10064  iccshftli  10066  iccdili  10068  icccntri  10070  fzdcel  10109  fznlem  10110  fzen  10112  fzofzim  10258  eluzgtdifelfzo  10267  elfzonelfzo  10300  qltnle  10316  addmodlteq  10472  qsqeqor  10724  apexp1  10792  fihashf1rn  10862  cjre  11029  caucvgre  11128  icodiamlt  11327  zsumdc  11530  zproddc  11725  reeff1  11846  dvdsmod0  11939  dvds2lem  11949  muldvds1  11962  dvdscmulr  11966  dvdsmulcr  11967  dvdsdivcl  11995  oddnn02np1  12024  ndvdsadd  12075  zeqzmulgcd  12110  bezoutlemmain  12138  dfgcd2  12154  gcdmultiple  12160  coprmdvds  12233  divgcdodd  12284  isprm6  12288  prmdvdsexpr  12291  cncongrprm  12298  phiprmpw  12363  modprm0  12395  pythagtriplem4  12409  pcz  12473  difsqpwdvds  12479  pcadd  12481  1arith  12508  isgrpid2  13115  ghmghmrn  13336  ghmf1  13346  kerf1ghm  13347  imasabl  13409  ringinvnz1ne0  13548  subrngringnsg  13704  domnmuln0  13772  rnglidlmcl  13979  znf1o  14150  znidom  14156  lmss  14425  cnplimcim  14846  dvcn  14879  gausslemma2dlem1a  15215  lgseisenlem2  15228  lgsquad2  15240  2lgslem1b  15246  2sqlem6  15277  ch2var  15329  bj-rspgt  15348  bj-charfundcALT  15371  bj-nntrans  15513  bj-nnelirr  15515  bj-omtrans  15518  setindft  15527  bj-inf2vnlem3  15534  bj-inf2vnlem4  15535  bj-findis  15541  pw1nct  15563