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  4247  exmidsssnc  4248  copsexg  4289  euotd  4300  rexxfrd  4511  relop  4829  elres  4996  rnxpid  5118  relcnvtr  5203  iotaval  5244  mpteqb  5672  elfvmptrab  5677  chfnrn  5693  elpreima  5701  ffnfv  5740  f1elima  5844  f1eqcocnv  5862  fliftfun  5867  isoresbr  5880  isotr  5887  ovmpodv2  6081  smoiso  6390  nnaordi  6596  nnaword  6599  nnawordi  6603  xpider  6695  iinerm  6696  mptelixpg  6823  dom2lem  6865  nneneq  6956  exmidpw  7007  infidc  7038  f1dmvrnfibi  7048  ismkvnex  7259  pr2nelem  7301  exmidfodomrlemeldju  7309  exmidfodomrlemreseldju  7310  netap  7368  2omotaplemap  7371  addcanpig  7449  mulcanpig  7450  enqer  7473  ltexnqi  7524  prarloclemlo  7609  genpcdl  7634  genpcuu  7635  appdivnq  7678  ltprordil  7704  1idprl  7705  1idpru  7706  ltexprlemm  7715  ltexprlemopu  7718  ltexprlemru  7727  cauappcvgprlemladdru  7771  cauappcvgprlemladdrl  7772  caucvgprprlemopu  7814  caucvgsrlemoffcau  7913  caucvgsrlemoffres  7915  ltrenn  7970  axpre-ltadd  8001  addn0nid  8448  apne  8698  aptap  8725  prodgt02  8928  prodge02  8930  mulgt1  8938  divgt0  8947  divge0  8948  cju  9036  nnsub  9077  nominpos  9277  zltnle  9420  nn0n0n1ge2  9445  zdcle  9451  btwnnz  9469  uzm1  9681  supinfneg  9718  infsupneg  9719  ublbneg  9736  cnref1o  9774  ltsubrp  9814  ltaddrp  9815  xnn0dcle  9926  npnflt  9939  nmnfgt  9942  ge0nemnf  9948  xltnegi  9959  xnn0xadd0  9991  iccsupr  10090  icoshft  10114  iccshftri  10119  iccshftli  10121  iccdili  10123  icccntri  10125  fzdcel  10164  fznlem  10165  fzen  10167  fzofzim  10314  eluzgtdifelfzo  10328  elfzonelfzo  10361  qltnle  10388  addmodlteq  10545  qsqeqor  10797  apexp1  10865  fihashf1rn  10935  lswlgt0cl  11048  pfxfv  11138  pfxsuff1eqwrdeq  11153  cjre  11226  caucvgre  11325  icodiamlt  11524  zsumdc  11728  zproddc  11923  reeff1  12044  dvdsmod0  12137  dvds2lem  12147  muldvds1  12160  dvdscmulr  12164  dvdsmulcr  12165  dvdsdivcl  12194  oddnn02np1  12224  ndvdsadd  12275  bitsinv1lem  12305  zeqzmulgcd  12324  bezoutlemmain  12352  dfgcd2  12368  gcdmultiple  12374  coprmdvds  12447  divgcdodd  12498  isprm6  12502  prmdvdsexpr  12505  cncongrprm  12512  phiprmpw  12577  modprm0  12610  pythagtriplem4  12624  pcz  12688  difsqpwdvds  12694  pcadd  12696  1arith  12723  isgrpid2  13405  ghmghmrn  13632  ghmf1  13642  kerf1ghm  13643  imasabl  13705  ringinvnz1ne0  13844  subrngringnsg  14000  domnmuln0  14068  rnglidlmcl  14275  znf1o  14446  znidom  14452  lmss  14751  cnplimcim  15172  dvcn  15205  fsumdvdsmul  15496  gausslemma2dlem1a  15568  lgseisenlem2  15581  lgsquad2  15593  2lgslem1b  15599  2sqlem6  15630  ch2var  15740  bj-rspgt  15759  bj-charfundcALT  15782  bj-nntrans  15924  bj-nnelirr  15926  bj-omtrans  15929  setindft  15938  bj-inf2vnlem3  15945  bj-inf2vnlem4  15946  bj-findis  15952  pw1nct  15977