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 ) )

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpbid  147  sylibd  149  sylbid  150  mpbidi  151  imbitrid  154  biimtrdi  163  ibi  176  imbi1d  231  biimpa  296  mtbird  677  mtbiri  679  orbi2d  795  pm5.15dc  1431  exlimd2  1641  exintr  1680  19.9d  1707  19.23t  1723  chvarfv  1746  dral1  1776  spimt  1782  cbvalv1  1797  cbvalh  1799  chvar  1803  exdistrfor  1846  sbequi  1885  spv  1906  cbvexvw  1967  eqrdav  2228  cleqh  2329  ceqsalg  2828  vtoclf  2854  vtocl2  2856  vtocl3  2857  spcdv  2888  rspcdv  2910  elabgt  2944  sbcn1  3076  sbcim1  3077  sbcbi1  3078  sbeqalb  3085  sbcel21v  3093  eqrd  3242  exmidsssn  4286  exmidsssnc  4287  copsexg  4330  euotd  4341  rexxfrd  4554  relop  4872  reldmm  4942  elres  5041  rnxpid  5163  relcnvtr  5248  iotaval  5290  mpteqb  5725  elfvmptrab  5730  chfnrn  5746  elpreima  5754  ffnfv  5793  f1elima  5897  f1eqcocnv  5915  fliftfun  5920  isoresbr  5933  isotr  5940  ovmpodv2  6138  smoiso  6448  nnaordi  6654  nnaword  6657  nnawordi  6661  xpider  6753  iinerm  6754  mptelixpg  6881  dom2lem  6923  nneneq  7018  exmidpw  7070  infidc  7101  f1dmvrnfibi  7111  ismkvnex  7322  pr2nelem  7364  exmidfodomrlemeldju  7377  exmidfodomrlemreseldju  7378  netap  7440  2omotaplemap  7443  addcanpig  7521  mulcanpig  7522  enqer  7545  ltexnqi  7596  prarloclemlo  7681  genpcdl  7706  genpcuu  7707  appdivnq  7750  ltprordil  7776  1idprl  7777  1idpru  7778  ltexprlemm  7787  ltexprlemopu  7790  ltexprlemru  7799  cauappcvgprlemladdru  7843  cauappcvgprlemladdrl  7844  caucvgprprlemopu  7886  caucvgsrlemoffcau  7985  caucvgsrlemoffres  7987  ltrenn  8042  axpre-ltadd  8073  addn0nid  8520  apne  8770  aptap  8797  prodgt02  9000  prodge02  9002  mulgt1  9010  divgt0  9019  divge0  9020  cju  9108  nnsub  9149  nominpos  9349  zltnle  9492  nn0n0n1ge2  9517  zdcle  9523  btwnnz  9541  uzm1  9753  supinfneg  9790  infsupneg  9791  ublbneg  9808  cnref1o  9846  ltsubrp  9886  ltaddrp  9887  xnn0dcle  9998  npnflt  10011  nmnfgt  10014  ge0nemnf  10020  xltnegi  10031  xnn0xadd0  10063  iccsupr  10162  icoshft  10186  iccshftri  10191  iccshftli  10193  iccdili  10195  icccntri  10197  fzdcel  10236  fznlem  10237  fzen  10239  fzofzim  10388  eluzgtdifelfzo  10403  elfzonelfzo  10436  qltnle  10463  addmodlteq  10620  qsqeqor  10872  apexp1  10940  fihashf1rn  11010  lswlgt0cl  11124  pfxfv  11216  pfxsuff1eqwrdeq  11231  ccatopth2  11249  swrdccat  11267  swrdccat3blem  11271  reuccatpfxs1lem  11278  cjre  11393  caucvgre  11492  icodiamlt  11691  zsumdc  11895  zproddc  12090  reeff1  12211  dvdsmod0  12304  dvds2lem  12314  muldvds1  12327  dvdscmulr  12331  dvdsmulcr  12332  dvdsdivcl  12361  oddnn02np1  12391  ndvdsadd  12442  bitsinv1lem  12472  zeqzmulgcd  12491  bezoutlemmain  12519  dfgcd2  12535  gcdmultiple  12541  coprmdvds  12614  divgcdodd  12665  isprm6  12669  prmdvdsexpr  12672  cncongrprm  12679  phiprmpw  12744  modprm0  12777  pythagtriplem4  12791  pcz  12855  difsqpwdvds  12861  pcadd  12863  1arith  12890  isgrpid2  13573  ghmghmrn  13800  ghmf1  13810  kerf1ghm  13811  imasabl  13873  ringinvnz1ne0  14012  subrngringnsg  14169  domnmuln0  14237  rnglidlmcl  14444  znf1o  14615  znidom  14621  lmss  14920  cnplimcim  15341  dvcn  15374  fsumdvdsmul  15665  gausslemma2dlem1a  15737  lgseisenlem2  15750  lgsquad2  15762  2lgslem1b  15768  2sqlem6  15799  upgrpredgv  15944  upgredgpr  15947  wlkpropg  16037  upgrwlkcompim  16073  uspgr2wlkeq  16076  wlklenvclwlk  16084  ch2var  16131  bj-rspgt  16150  bj-charfundcALT  16172  bj-nntrans  16314  bj-nnelirr  16316  bj-omtrans  16319  setindft  16328  bj-inf2vnlem3  16335  bj-inf2vnlem4  16336  bj-findis  16342  pw1nct  16369