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  675  mtbiri  677  orbi2d  792  pm5.15dc  1409  exlimd2  1618  exintr  1657  19.9d  1684  19.23t  1700  chvarfv  1723  dral1  1753  spimt  1759  cbvalv1  1774  cbvalh  1776  chvar  1780  exdistrfor  1823  sbequi  1862  spv  1883  cbvexvw  1944  eqrdav  2204  cleqh  2305  ceqsalg  2800  vtoclf  2826  vtocl2  2828  vtocl3  2829  spcdv  2858  rspcdv  2880  elabgt  2914  sbcn1  3046  sbcim1  3047  sbcbi1  3048  sbeqalb  3055  sbcel21v  3063  eqrd  3211  exmidsssn  4246  exmidsssnc  4247  copsexg  4288  euotd  4299  rexxfrd  4510  relop  4828  elres  4995  rnxpid  5117  relcnvtr  5202  iotaval  5243  mpteqb  5670  elfvmptrab  5675  chfnrn  5691  elpreima  5699  ffnfv  5738  f1elima  5842  f1eqcocnv  5860  fliftfun  5865  isoresbr  5878  isotr  5885  ovmpodv2  6079  smoiso  6388  nnaordi  6594  nnaword  6597  nnawordi  6601  xpider  6693  iinerm  6694  mptelixpg  6821  dom2lem  6863  nneneq  6954  exmidpw  7005  infidc  7036  f1dmvrnfibi  7046  ismkvnex  7257  pr2nelem  7299  exmidfodomrlemeldju  7307  exmidfodomrlemreseldju  7308  netap  7366  2omotaplemap  7369  addcanpig  7447  mulcanpig  7448  enqer  7471  ltexnqi  7522  prarloclemlo  7607  genpcdl  7632  genpcuu  7633  appdivnq  7676  ltprordil  7702  1idprl  7703  1idpru  7704  ltexprlemm  7713  ltexprlemopu  7716  ltexprlemru  7725  cauappcvgprlemladdru  7769  cauappcvgprlemladdrl  7770  caucvgprprlemopu  7812  caucvgsrlemoffcau  7911  caucvgsrlemoffres  7913  ltrenn  7968  axpre-ltadd  7999  addn0nid  8446  apne  8696  aptap  8723  prodgt02  8926  prodge02  8928  mulgt1  8936  divgt0  8945  divge0  8946  cju  9034  nnsub  9075  nominpos  9275  zltnle  9418  nn0n0n1ge2  9443  zdcle  9449  btwnnz  9467  uzm1  9679  supinfneg  9716  infsupneg  9717  ublbneg  9734  cnref1o  9772  ltsubrp  9812  ltaddrp  9813  xnn0dcle  9924  npnflt  9937  nmnfgt  9940  ge0nemnf  9946  xltnegi  9957  xnn0xadd0  9989  iccsupr  10088  icoshft  10112  iccshftri  10117  iccshftli  10119  iccdili  10121  icccntri  10123  fzdcel  10162  fznlem  10163  fzen  10165  fzofzim  10312  eluzgtdifelfzo  10326  elfzonelfzo  10359  qltnle  10386  addmodlteq  10543  qsqeqor  10795  apexp1  10863  fihashf1rn  10933  lswlgt0cl  11045  cjre  11193  caucvgre  11292  icodiamlt  11491  zsumdc  11695  zproddc  11890  reeff1  12011  dvdsmod0  12104  dvds2lem  12114  muldvds1  12127  dvdscmulr  12131  dvdsmulcr  12132  dvdsdivcl  12161  oddnn02np1  12191  ndvdsadd  12242  bitsinv1lem  12272  zeqzmulgcd  12291  bezoutlemmain  12319  dfgcd2  12335  gcdmultiple  12341  coprmdvds  12414  divgcdodd  12465  isprm6  12469  prmdvdsexpr  12472  cncongrprm  12479  phiprmpw  12544  modprm0  12577  pythagtriplem4  12591  pcz  12655  difsqpwdvds  12661  pcadd  12663  1arith  12690  isgrpid2  13372  ghmghmrn  13599  ghmf1  13609  kerf1ghm  13610  imasabl  13672  ringinvnz1ne0  13811  subrngringnsg  13967  domnmuln0  14035  rnglidlmcl  14242  znf1o  14413  znidom  14419  lmss  14718  cnplimcim  15139  dvcn  15172  fsumdvdsmul  15463  gausslemma2dlem1a  15535  lgseisenlem2  15548  lgsquad2  15560  2lgslem1b  15566  2sqlem6  15597  ch2var  15707  bj-rspgt  15726  bj-charfundcALT  15749  bj-nntrans  15891  bj-nnelirr  15893  bj-omtrans  15896  setindft  15905  bj-inf2vnlem3  15912  bj-inf2vnlem4  15913  bj-findis  15919  pw1nct  15944