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		bi1 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  662  mtbiri  664  orbi2d  779  pm5.15dc  1367  exlimd2  1574  exintr  1613  19.9d  1639  19.23t  1655  dral1  1708  spimt  1714  cbvalh  1726  chvar  1730  exdistrfor  1772  sbequi  1811  spv  1832  eqrdav  2136  cleqh  2237  ceqsalg  2709  vtoclf  2734  vtocl2  2736  vtocl3  2737  spcdv  2766  rspcdv  2787  elabgt  2820  sbcn1  2951  sbcim1  2952  sbcbi1  2953  sbeqalb  2960  sbcel21v  2968  eqrd  3110  exmidsssn  4120  exmidsssnc  4121  copsexg  4161  euotd  4171  rexxfrd  4379  relop  4684  elres  4850  rnxpid  4968  relcnvtr  5053  iotaval  5094  mpteqb  5504  elfvmptrab  5509  chfnrn  5524  elpreima  5532  ffnfv  5571  f1elima  5667  f1eqcocnv  5685  fliftfun  5690  isoresbr  5703  isotr  5710  ovmpodv2  5897  smoiso  6192  nnaordi  6397  nnaword  6400  nnawordi  6404  xpider  6493  iinerm  6494  mptelixpg  6621  dom2lem  6659  nneneq  6744  exmidpw  6795  f1dmvrnfibi  6825  ismkvnex  7022  pr2nelem  7040  exmidfodomrlemeldju  7048  exmidfodomrlemreseldju  7049  addcanpig  7135  mulcanpig  7136  enqer  7159  ltexnqi  7210  prarloclemlo  7295  genpcdl  7320  genpcuu  7321  appdivnq  7364  ltprordil  7390  1idprl  7391  1idpru  7392  ltexprlemm  7401  ltexprlemopu  7404  ltexprlemru  7413  cauappcvgprlemladdru  7457  cauappcvgprlemladdrl  7458  caucvgprprlemopu  7500  caucvgsrlemoffcau  7599  caucvgsrlemoffres  7601  ltrenn  7656  axpre-ltadd  7687  addn0nid  8129  apne  8378  prodgt02  8604  prodge02  8606  mulgt1  8614  divgt0  8623  divge0  8624  cju  8712  nnsub  8752  nominpos  8950  zltnle  9093  nn0n0n1ge2  9114  zdcle  9120  btwnnz  9138  uzm1  9349  supinfneg  9383  infsupneg  9384  ublbneg  9398  cnref1o  9433  ltsubrp  9471  ltaddrp  9472  npnflt  9591  nmnfgt  9594  ge0nemnf  9600  xltnegi  9611  xnn0xadd0  9643  iccsupr  9742  icoshft  9766  iccshftri  9771  iccshftli  9773  iccdili  9775  icccntri  9777  fzdcel  9813  fznlem  9814  fzen  9816  fzofzim  9958  eluzgtdifelfzo  9967  elfzonelfzo  10000  qltnle  10016  addmodlteq  10164  fihashf1rn  10528  cjre  10647  caucvgre  10746  icodiamlt  10945  zsumdc  11146  reeff1  11396  dvds2lem  11494  muldvds1  11507  dvdscmulr  11511  dvdsmulcr  11512  dvdsdivcl  11537  oddnn02np1  11566  ndvdsadd  11617  zeqzmulgcd  11648  bezoutlemmain  11675  dfgcd2  11691  gcdmultiple  11697  coprmdvds  11762  divgcdodd  11810  isprm6  11814  prmdvdsexpr  11817  cncongrprm  11824  phiprmpw  11887  lmss  12404  cnplimcim  12794  dvcn  12822  ch2var  12963  bj-rspgt  12982  bj-nntrans  13138  bj-nnelirr  13140  bj-omtrans  13143  setindft  13152  bj-inf2vnlem3  13159  bj-inf2vnlem4  13160  bj-findis  13166