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  1379  exlimd2  1583  exintr  1622  19.9d  1649  19.23t  1665  chvarfv  1688  dral1  1718  spimt  1724  cbvalv1  1739  cbvalh  1741  chvar  1745  exdistrfor  1788  sbequi  1827  spv  1848  cbvexvw  1908  eqrdav  2164  cleqh  2265  ceqsalg  2753  vtoclf  2778  vtocl2  2780  vtocl3  2781  spcdv  2810  rspcdv  2832  elabgt  2866  sbcn1  2997  sbcim1  2998  sbcbi1  2999  sbeqalb  3006  sbcel21v  3014  eqrd  3159  exmidsssn  4180  exmidsssnc  4181  copsexg  4221  euotd  4231  rexxfrd  4440  relop  4753  elres  4919  rnxpid  5037  relcnvtr  5122  iotaval  5163  mpteqb  5575  elfvmptrab  5580  chfnrn  5595  elpreima  5603  ffnfv  5642  f1elima  5740  f1eqcocnv  5758  fliftfun  5763  isoresbr  5776  isotr  5783  ovmpodv2  5971  smoiso  6266  nnaordi  6472  nnaword  6475  nnawordi  6479  xpider  6568  iinerm  6569  mptelixpg  6696  dom2lem  6734  nneneq  6819  exmidpw  6870  f1dmvrnfibi  6905  ismkvnex  7115  pr2nelem  7143  exmidfodomrlemeldju  7151  exmidfodomrlemreseldju  7152  addcanpig  7271  mulcanpig  7272  enqer  7295  ltexnqi  7346  prarloclemlo  7431  genpcdl  7456  genpcuu  7457  appdivnq  7500  ltprordil  7526  1idprl  7527  1idpru  7528  ltexprlemm  7537  ltexprlemopu  7540  ltexprlemru  7549  cauappcvgprlemladdru  7593  cauappcvgprlemladdrl  7594  caucvgprprlemopu  7636  caucvgsrlemoffcau  7735  caucvgsrlemoffres  7737  ltrenn  7792  axpre-ltadd  7823  addn0nid  8268  apne  8517  prodgt02  8744  prodge02  8746  mulgt1  8754  divgt0  8763  divge0  8764  cju  8852  nnsub  8892  nominpos  9090  zltnle  9233  nn0n0n1ge2  9257  zdcle  9263  btwnnz  9281  uzm1  9492  supinfneg  9529  infsupneg  9530  ublbneg  9547  cnref1o  9584  ltsubrp  9622  ltaddrp  9623  xnn0dcle  9734  npnflt  9747  nmnfgt  9750  ge0nemnf  9756  xltnegi  9767  xnn0xadd0  9799  iccsupr  9898  icoshft  9922  iccshftri  9927  iccshftli  9929  iccdili  9931  icccntri  9933  fzdcel  9971  fznlem  9972  fzen  9974  fzofzim  10119  eluzgtdifelfzo  10128  elfzonelfzo  10161  qltnle  10177  addmodlteq  10329  qsqeqor  10561  apexp1  10627  fihashf1rn  10698  cjre  10820  caucvgre  10919  icodiamlt  11118  zsumdc  11321  zproddc  11516  reeff1  11637  dvdsmod0  11729  dvds2lem  11739  muldvds1  11752  dvdscmulr  11756  dvdsmulcr  11757  dvdsdivcl  11784  oddnn02np1  11813  ndvdsadd  11864  zeqzmulgcd  11899  bezoutlemmain  11927  dfgcd2  11943  gcdmultiple  11949  coprmdvds  12020  divgcdodd  12071  isprm6  12075  prmdvdsexpr  12078  cncongrprm  12085  phiprmpw  12150  modprm0  12182  pythagtriplem4  12196  pcz  12259  difsqpwdvds  12265  pcadd  12267  1arith  12293  lmss  12846  cnplimcim  13236  dvcn  13264  2sqlem6  13556  ch2var  13608  bj-rspgt  13627  bj-charfundcALT  13651  bj-nntrans  13793  bj-nnelirr  13795  bj-omtrans  13798  setindft  13807  bj-inf2vnlem3  13814  bj-inf2vnlem4  13815  bj-findis  13821  pw1nct  13843