Theorem biimpd 143

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 117	. 2 |- ( ( ps <-> ch ) -> ( ps -> ch ) )
3	1, 2	syl 14	1 |- ( ph -> ( ps -> ch ) )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpbid  146  sylibd  148  sylbid  149  mpbidi  150  syl5ib  153  syl6bi  162  ibi  175  imbi1d  230  biimpa  294  mtbird  668  mtbiri  670  orbi2d  785  pm5.15dc  1384  exlimd2  1588  exintr  1627  19.9d  1654  19.23t  1670  chvarfv  1693  dral1  1723  spimt  1729  cbvalv1  1744  cbvalh  1746  chvar  1750  exdistrfor  1793  sbequi  1832  spv  1853  cbvexvw  1913  eqrdav  2169  cleqh  2270  ceqsalg  2758  vtoclf  2783  vtocl2  2785  vtocl3  2786  spcdv  2815  rspcdv  2837  elabgt  2871  sbcn1  3002  sbcim1  3003  sbcbi1  3004  sbeqalb  3011  sbcel21v  3019  eqrd  3165  exmidsssn  4188  exmidsssnc  4189  copsexg  4229  euotd  4239  rexxfrd  4448  relop  4761  elres  4927  rnxpid  5045  relcnvtr  5130  iotaval  5171  mpteqb  5586  elfvmptrab  5591  chfnrn  5607  elpreima  5615  ffnfv  5654  f1elima  5752  f1eqcocnv  5770  fliftfun  5775  isoresbr  5788  isotr  5795  ovmpodv2  5986  smoiso  6281  nnaordi  6487  nnaword  6490  nnawordi  6494  xpider  6584  iinerm  6585  mptelixpg  6712  dom2lem  6750  nneneq  6835  exmidpw  6886  f1dmvrnfibi  6921  ismkvnex  7131  pr2nelem  7168  exmidfodomrlemeldju  7176  exmidfodomrlemreseldju  7177  addcanpig  7296  mulcanpig  7297  enqer  7320  ltexnqi  7371  prarloclemlo  7456  genpcdl  7481  genpcuu  7482  appdivnq  7525  ltprordil  7551  1idprl  7552  1idpru  7553  ltexprlemm  7562  ltexprlemopu  7565  ltexprlemru  7574  cauappcvgprlemladdru  7618  cauappcvgprlemladdrl  7619  caucvgprprlemopu  7661  caucvgsrlemoffcau  7760  caucvgsrlemoffres  7762  ltrenn  7817  axpre-ltadd  7848  addn0nid  8293  apne  8542  prodgt02  8769  prodge02  8771  mulgt1  8779  divgt0  8788  divge0  8789  cju  8877  nnsub  8917  nominpos  9115  zltnle  9258  nn0n0n1ge2  9282  zdcle  9288  btwnnz  9306  uzm1  9517  supinfneg  9554  infsupneg  9555  ublbneg  9572  cnref1o  9609  ltsubrp  9647  ltaddrp  9648  xnn0dcle  9759  npnflt  9772  nmnfgt  9775  ge0nemnf  9781  xltnegi  9792  xnn0xadd0  9824  iccsupr  9923  icoshft  9947  iccshftri  9952  iccshftli  9954  iccdili  9956  icccntri  9958  fzdcel  9996  fznlem  9997  fzen  9999  fzofzim  10144  eluzgtdifelfzo  10153  elfzonelfzo  10186  qltnle  10202  addmodlteq  10354  qsqeqor  10586  apexp1  10652  fihashf1rn  10723  cjre  10846  caucvgre  10945  icodiamlt  11144  zsumdc  11347  zproddc  11542  reeff1  11663  dvdsmod0  11755  dvds2lem  11765  muldvds1  11778  dvdscmulr  11782  dvdsmulcr  11783  dvdsdivcl  11810  oddnn02np1  11839  ndvdsadd  11890  zeqzmulgcd  11925  bezoutlemmain  11953  dfgcd2  11969  gcdmultiple  11975  coprmdvds  12046  divgcdodd  12097  isprm6  12101  prmdvdsexpr  12104  cncongrprm  12111  phiprmpw  12176  modprm0  12208  pythagtriplem4  12222  pcz  12285  difsqpwdvds  12291  pcadd  12293  1arith  12319  isgrpid2  12743  lmss  13040  cnplimcim  13430  dvcn  13458  2sqlem6  13750  ch2var  13802  bj-rspgt  13821  bj-charfundcALT  13844  bj-nntrans  13986  bj-nnelirr  13988  bj-omtrans  13991  setindft  14000  bj-inf2vnlem3  14007  bj-inf2vnlem4  14008  bj-findis  14014  pw1nct  14036