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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used by:  mpbid  147  sylibd  149  sylbid  150  mpbidi  151  imbitrid  154  biimtrdi  163  ibi  176  imbi1d  231  biimpa  296  mtbird  684  mtbiri  686  orbi2d  802  pm5.15dc  1438  exlimd2  1648  exintr  1687  19.9d  1713  19.23t  1729  chvarfv  1752  dral1  1783  spimt  1789  cbvalv1  1804  cbvalh  1806  chvar  1810  exdistrfor  1853  sbequi  1892  spv  1913  cbvexvw  1976  eqrdav  2237  cleqh  2338  ceqsalg  2850  vtoclf  2876  vtocl2  2878  vtocl3  2879  spcdv  2910  rspcdv  2932  elabgt  2967  sbcn1  3099  sbcim1  3100  sbcbi1  3101  sbeqalb  3108  sbcel21v  3116  eqrd  3266  ifeqeqxdc  3687  rabsnifsb  3777  exmidsssn  4341  exmidsssnc  4342  copsexg  4386  euotd  4397  rexxfrd  4611  relop  4932  reldmm  5002  elres  5101  rnxpid  5225  relcnvtr  5310  iotaval  5352  mpteqb  5799  elfvmptrab  5805  chfnrn  5823  elpreima  5831  ffnfv  5869  f1elima  5982  f1eqcocnv  6000  fliftfun  6005  isoresbr  6018  isotr  6025  ovmpodv2  6225  ressuppss  6498  funsssuppss  6502  smoiso  6578  nnaordi  6786  nnaword  6789  nnawordi  6793  xpider  6885  iinerm  6886  mptelixpg  7022  dom2lem  7064  nneneq  7164  exmidpw  7221  infidc  7254  f1dmvrnfibi  7264  ismkvnex  7501  pr2nelem  7543  exmidfodomrlemeldju  7557  exmidfodomrlemreseldju  7558  netap  7626  2omotaplemap  7629  addcanpig  7707  mulcanpig  7708  enqer  7731  ltexnqi  7782  prarloclemlo  7867  genpcdl  7892  genpcuu  7893  appdivnq  7936  ltprordil  7962  1idprl  7963  1idpru  7964  ltexprlemm  7973  ltexprlemopu  7976  ltexprlemru  7985  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  caucvgprprlemopu  8072  caucvgsrlemoffcau  8171  caucvgsrlemoffres  8173  ltrenn  8228  axpre-ltadd  8259  addn0nid  8707  apne  8959  aptap  8986  prodgt02  9191  prodge02  9193  mulgt1  9201  divgt0  9210  divge0  9211  cju  9299  nnsub  9352  nominpos  9554  zltnle  9699  nn0n0n1ge2  9724  zdcle  9730  btwnnz  9750  uzm1  9968  supinfneg  10010  infsupneg  10011  ublbneg  10028  cnref1o  10067  ltsubrp  10107  ltaddrp  10108  xnn0dcle  10220  npnflt  10233  nmnfgt  10236  ge0nemnf  10242  xltnegi  10253  xnn0xadd0  10285  iccsupr  10384  icoshft  10408  iccshftri  10413  iccshftli  10415  iccdili  10417  icccntri  10419  fzdcel  10460  fznlem  10461  fzen  10463  fzofzim  10616  eluzgtdifelfzo  10631  elfzonelfzo  10664  qltnle  10694  addmodlteq  10855  qsqeqor  11107  apexp1  11177  fihashf1rn  11248  lswlgt0cl  11378  ccatalpha  11402  pfxfv  11477  pfxsuff1eqwrdeq  11492  ccatopth2  11510  swrdccat  11528  swrdccat3blem  11532  reuccatpfxs1lem  11539  cjre  11668  caucvgre  11768  icodiamlt  11968  zsumdc  12175  zproddc  12370  reeff1  12491  dvdsmod0  12584  dvds2lem  12594  muldvds1  12607  dvdscmulr  12611  dvdsmulcr  12612  dvdsdivcl  12641  oddnn02np1  12671  ndvdsadd  12722  bitsinv1lem  12752  zeqzmulgcd  12771  bezoutlemmain  12799  dfgcd2  12815  gcdmultiple  12821  coprmdvds  12894  divgcdodd  12946  isprm6  12950  prmdvdsexpr  12953  cncongrprm  12960  phiprmpw  13028  modprm0  13061  pythagtriplem4  13075  pcz  13139  difsqpwdvds  13145  pcadd  13147  1arith  13174  ballotfilemfc0  13289  ballotfilemfcc  13290  isgrpid2  13903  ghmghmrn  14124  ghmf1  14134  kerf1ghm  14135  imasabl  14229  rng1zrlem  14364  ringinvnz1ne0  14460  subrngringnsg  14621  domnmuln0  14690  rnglidlmcl  14925  znf1o  15094  znidom  15100  lmss  15489  cnplimcim  15910  dvcn  15943  fsumdvdsmul  16302  bposlem7  16334  gausslemma2dlem1a  16399  lgseisenlem2  16412  lgsquad2  16424  2lgslem1b  16430  2sqlem6  16461  upgrpredgv  16609  upgredgpr  16612  uhgr0v0e  16697  subgrprop  16722  wlkpropg  16787  upgrwlkcompim  16825  uspgr2wlkeq  16828  wlklenvclwlk  16836  wlkres  16842  clwwlk1loop  16862  umgrclwwlkge2  16865  clwwlkn1loopb  16883  clwwlknonex2lem2  16901  ch2var  17017  bj-rspgt  17036  bj-charfundcALT  17057  bj-nntrans  17199  bj-nnelirr  17201  bj-omtrans  17204  setindft  17213  bj-inf2vnlem3  17220  bj-inf2vnlem4  17221  bj-findis  17227  pw1nct  17255