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  4339  exmidsssnc  4340  copsexg  4384  euotd  4395  rexxfrd  4609  relop  4930  reldmm  5000  elres  5099  rnxpid  5222  relcnvtr  5307  iotaval  5349  mpteqb  5796  elfvmptrab  5802  chfnrn  5820  elpreima  5828  ffnfv  5866  f1elima  5979  f1eqcocnv  5997  fliftfun  6002  isoresbr  6015  isotr  6022  ovmpodv2  6222  ressuppss  6494  funsssuppss  6498  smoiso  6573  nnaordi  6781  nnaword  6784  nnawordi  6788  xpider  6880  iinerm  6881  mptelixpg  7016  dom2lem  7058  nneneq  7158  exmidpw  7215  infidc  7248  f1dmvrnfibi  7258  fsuppimp  7292  ismkvnex  7495  pr2nelem  7537  exmidfodomrlemeldju  7551  exmidfodomrlemreseldju  7552  netap  7620  2omotaplemap  7623  addcanpig  7701  mulcanpig  7702  enqer  7725  ltexnqi  7776  prarloclemlo  7861  genpcdl  7886  genpcuu  7887  appdivnq  7930  ltprordil  7956  1idprl  7957  1idpru  7958  ltexprlemm  7967  ltexprlemopu  7970  ltexprlemru  7979  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  caucvgprprlemopu  8066  caucvgsrlemoffcau  8165  caucvgsrlemoffres  8167  ltrenn  8222  axpre-ltadd  8253  addn0nid  8700  apne  8951  aptap  8978  prodgt02  9183  prodge02  9185  mulgt1  9193  divgt0  9202  divge0  9203  cju  9291  nnsub  9343  nominpos  9543  zltnle  9690  nn0n0n1ge2  9715  zdcle  9721  btwnnz  9740  uzm1  9953  supinfneg  9995  infsupneg  9996  ublbneg  10013  cnref1o  10051  ltsubrp  10091  ltaddrp  10092  xnn0dcle  10204  npnflt  10217  nmnfgt  10220  ge0nemnf  10226  xltnegi  10237  xnn0xadd0  10269  iccsupr  10368  icoshft  10392  iccshftri  10397  iccshftli  10399  iccdili  10401  icccntri  10403  fzdcel  10444  fznlem  10445  fzen  10447  fzofzim  10600  eluzgtdifelfzo  10615  elfzonelfzo  10648  qltnle  10678  addmodlteq  10835  qsqeqor  11087  apexp1  11156  fihashf1rn  11227  lswlgt0cl  11357  ccatalpha  11381  pfxfv  11456  pfxsuff1eqwrdeq  11471  ccatopth2  11489  swrdccat  11507  swrdccat3blem  11511  reuccatpfxs1lem  11518  cjre  11647  caucvgre  11747  icodiamlt  11946  zsumdc  12151  zproddc  12346  reeff1  12467  dvdsmod0  12560  dvds2lem  12570  muldvds1  12583  dvdscmulr  12587  dvdsmulcr  12588  dvdsdivcl  12617  oddnn02np1  12647  ndvdsadd  12698  bitsinv1lem  12728  zeqzmulgcd  12747  bezoutlemmain  12775  dfgcd2  12791  gcdmultiple  12797  coprmdvds  12870  divgcdodd  12921  isprm6  12925  prmdvdsexpr  12928  cncongrprm  12935  phiprmpw  13000  modprm0  13033  pythagtriplem4  13047  pcz  13111  difsqpwdvds  13117  pcadd  13119  1arith  13146  ballotfilemfc0  13232  ballotfilemfcc  13233  isgrpid2  13845  ghmghmrn  14066  ghmf1  14076  kerf1ghm  14077  imasabl  14140  rng1zrlem  14258  ringinvnz1ne0  14354  subrngringnsg  14513  domnmuln0  14582  rnglidlmcl  14817  znf1o  14986  znidom  14992  lmss  15347  cnplimcim  15768  dvcn  15801  fsumdvdsmul  16105  gausslemma2dlem1a  16177  lgseisenlem2  16190  lgsquad2  16202  2lgslem1b  16208  2sqlem6  16239  upgrpredgv  16387  upgredgpr  16390  uhgr0v0e  16475  subgrprop  16500  wlkpropg  16565  upgrwlkcompim  16603  uspgr2wlkeq  16606  wlklenvclwlk  16614  wlkres  16620  clwwlk1loop  16640  umgrclwwlkge2  16643  clwwlkn1loopb  16661  clwwlknonex2lem2  16679  ch2var  16795  bj-rspgt  16814  bj-charfundcALT  16835  bj-nntrans  16977  bj-nnelirr  16979  bj-omtrans  16982  setindft  16991  bj-inf2vnlem3  16998  bj-inf2vnlem4  16999  bj-findis  17005  pw1nct  17033