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  1609  exintr  1648  19.9d  1675  19.23t  1691  chvarfv  1714  dral1  1744  spimt  1750  cbvalv1  1765  cbvalh  1767  chvar  1771  exdistrfor  1814  sbequi  1853  spv  1874  cbvexvw  1935  eqrdav  2195  cleqh  2296  ceqsalg  2791  vtoclf  2817  vtocl2  2819  vtocl3  2820  spcdv  2849  rspcdv  2871  elabgt  2905  sbcn1  3037  sbcim1  3038  sbcbi1  3039  sbeqalb  3046  sbcel21v  3054  eqrd  3201  exmidsssn  4235  exmidsssnc  4236  copsexg  4277  euotd  4287  rexxfrd  4498  relop  4816  elres  4982  rnxpid  5104  relcnvtr  5189  iotaval  5230  mpteqb  5652  elfvmptrab  5657  chfnrn  5673  elpreima  5681  ffnfv  5720  f1elima  5820  f1eqcocnv  5838  fliftfun  5843  isoresbr  5856  isotr  5863  ovmpodv2  6056  smoiso  6360  nnaordi  6566  nnaword  6569  nnawordi  6573  xpider  6665  iinerm  6666  mptelixpg  6793  dom2lem  6831  nneneq  6918  exmidpw  6969  infidc  7000  f1dmvrnfibi  7010  ismkvnex  7221  pr2nelem  7258  exmidfodomrlemeldju  7266  exmidfodomrlemreseldju  7267  netap  7321  2omotaplemap  7324  addcanpig  7401  mulcanpig  7402  enqer  7425  ltexnqi  7476  prarloclemlo  7561  genpcdl  7586  genpcuu  7587  appdivnq  7630  ltprordil  7656  1idprl  7657  1idpru  7658  ltexprlemm  7667  ltexprlemopu  7670  ltexprlemru  7679  cauappcvgprlemladdru  7723  cauappcvgprlemladdrl  7724  caucvgprprlemopu  7766  caucvgsrlemoffcau  7865  caucvgsrlemoffres  7867  ltrenn  7922  axpre-ltadd  7953  addn0nid  8400  apne  8650  aptap  8677  prodgt02  8880  prodge02  8882  mulgt1  8890  divgt0  8899  divge0  8900  cju  8988  nnsub  9029  nominpos  9229  zltnle  9372  nn0n0n1ge2  9396  zdcle  9402  btwnnz  9420  uzm1  9632  supinfneg  9669  infsupneg  9670  ublbneg  9687  cnref1o  9725  ltsubrp  9765  ltaddrp  9766  xnn0dcle  9877  npnflt  9890  nmnfgt  9893  ge0nemnf  9899  xltnegi  9910  xnn0xadd0  9942  iccsupr  10041  icoshft  10065  iccshftri  10070  iccshftli  10072  iccdili  10074  icccntri  10076  fzdcel  10115  fznlem  10116  fzen  10118  fzofzim  10264  eluzgtdifelfzo  10273  elfzonelfzo  10306  qltnle  10333  addmodlteq  10490  qsqeqor  10742  apexp1  10810  fihashf1rn  10880  cjre  11047  caucvgre  11146  icodiamlt  11345  zsumdc  11549  zproddc  11744  reeff1  11865  dvdsmod0  11958  dvds2lem  11968  muldvds1  11981  dvdscmulr  11985  dvdsmulcr  11986  dvdsdivcl  12015  oddnn02np1  12045  ndvdsadd  12096  zeqzmulgcd  12137  bezoutlemmain  12165  dfgcd2  12181  gcdmultiple  12187  coprmdvds  12260  divgcdodd  12311  isprm6  12315  prmdvdsexpr  12318  cncongrprm  12325  phiprmpw  12390  modprm0  12423  pythagtriplem4  12437  pcz  12501  difsqpwdvds  12507  pcadd  12509  1arith  12536  isgrpid2  13172  ghmghmrn  13393  ghmf1  13403  kerf1ghm  13404  imasabl  13466  ringinvnz1ne0  13605  subrngringnsg  13761  domnmuln0  13829  rnglidlmcl  14036  znf1o  14207  znidom  14213  lmss  14482  cnplimcim  14903  dvcn  14936  fsumdvdsmul  15227  gausslemma2dlem1a  15299  lgseisenlem2  15312  lgsquad2  15324  2lgslem1b  15330  2sqlem6  15361  ch2var  15413  bj-rspgt  15432  bj-charfundcALT  15455  bj-nntrans  15597  bj-nnelirr  15599  bj-omtrans  15602  setindft  15611  bj-inf2vnlem3  15618  bj-inf2vnlem4  15619  bj-findis  15625  pw1nct  15647