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  663  mtbiri  665  orbi2d  780  pm5.15dc  1371  exlimd2  1575  exintr  1614  19.9d  1641  19.23t  1657  chvarfv  1680  dral1  1710  spimt  1716  cbvalv1  1731  cbvalh  1733  chvar  1737  exdistrfor  1780  sbequi  1819  spv  1840  cbvexvw  1900  eqrdav  2156  cleqh  2257  ceqsalg  2740  vtoclf  2765  vtocl2  2767  vtocl3  2768  spcdv  2797  rspcdv  2819  elabgt  2853  sbcn1  2984  sbcim1  2985  sbcbi1  2986  sbeqalb  2993  sbcel21v  3001  eqrd  3146  exmidsssn  4163  exmidsssnc  4164  copsexg  4204  euotd  4214  rexxfrd  4423  relop  4736  elres  4902  rnxpid  5020  relcnvtr  5105  iotaval  5146  mpteqb  5558  elfvmptrab  5563  chfnrn  5578  elpreima  5586  ffnfv  5625  f1elima  5723  f1eqcocnv  5741  fliftfun  5746  isoresbr  5759  isotr  5766  ovmpodv2  5954  smoiso  6249  nnaordi  6455  nnaword  6458  nnawordi  6462  xpider  6551  iinerm  6552  mptelixpg  6679  dom2lem  6717  nneneq  6802  exmidpw  6853  f1dmvrnfibi  6888  ismkvnex  7098  pr2nelem  7126  exmidfodomrlemeldju  7134  exmidfodomrlemreseldju  7135  addcanpig  7254  mulcanpig  7255  enqer  7278  ltexnqi  7329  prarloclemlo  7414  genpcdl  7439  genpcuu  7440  appdivnq  7483  ltprordil  7509  1idprl  7510  1idpru  7511  ltexprlemm  7520  ltexprlemopu  7523  ltexprlemru  7532  cauappcvgprlemladdru  7576  cauappcvgprlemladdrl  7577  caucvgprprlemopu  7619  caucvgsrlemoffcau  7718  caucvgsrlemoffres  7720  ltrenn  7775  axpre-ltadd  7806  addn0nid  8249  apne  8498  prodgt02  8724  prodge02  8726  mulgt1  8734  divgt0  8743  divge0  8744  cju  8832  nnsub  8872  nominpos  9070  zltnle  9213  nn0n0n1ge2  9234  zdcle  9240  btwnnz  9258  uzm1  9469  supinfneg  9506  infsupneg  9507  ublbneg  9522  cnref1o  9559  ltsubrp  9597  ltaddrp  9598  npnflt  9719  nmnfgt  9722  ge0nemnf  9728  xltnegi  9739  xnn0xadd0  9771  iccsupr  9870  icoshft  9894  iccshftri  9899  iccshftli  9901  iccdili  9903  icccntri  9905  fzdcel  9942  fznlem  9943  fzen  9945  fzofzim  10087  eluzgtdifelfzo  10096  elfzonelfzo  10129  qltnle  10145  addmodlteq  10297  apexp1  10592  fihashf1rn  10663  cjre  10782  caucvgre  10881  icodiamlt  11080  zsumdc  11281  zproddc  11476  reeff1  11597  dvdsmod0  11689  dvds2lem  11699  muldvds1  11712  dvdscmulr  11716  dvdsmulcr  11717  dvdsdivcl  11742  oddnn02np1  11771  ndvdsadd  11822  zeqzmulgcd  11854  bezoutlemmain  11882  dfgcd2  11898  gcdmultiple  11904  coprmdvds  11969  divgcdodd  12018  isprm6  12022  prmdvdsexpr  12025  cncongrprm  12032  phiprmpw  12097  modprm0  12129  lmss  12657  cnplimcim  13047  dvcn  13075  ch2var  13352  bj-rspgt  13371  bj-charfundcALT  13395  bj-nntrans  13537  bj-nnelirr  13539  bj-omtrans  13542  setindft  13551  bj-inf2vnlem3  13558  bj-inf2vnlem4  13559  bj-findis  13565  pw1nct  13586