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  syl6bi  163  ibi  176  imbi1d  231  biimpa  296  mtbird  673  mtbiri  675  orbi2d  790  pm5.15dc  1389  exlimd2  1595  exintr  1634  19.9d  1661  19.23t  1677  chvarfv  1700  dral1  1730  spimt  1736  cbvalv1  1751  cbvalh  1753  chvar  1757  exdistrfor  1800  sbequi  1839  spv  1860  cbvexvw  1920  eqrdav  2176  cleqh  2277  ceqsalg  2765  vtoclf  2790  vtocl2  2792  vtocl3  2793  spcdv  2822  rspcdv  2844  elabgt  2878  sbcn1  3010  sbcim1  3011  sbcbi1  3012  sbeqalb  3019  sbcel21v  3027  eqrd  3173  exmidsssn  4202  exmidsssnc  4203  copsexg  4244  euotd  4254  rexxfrd  4463  relop  4777  elres  4943  rnxpid  5063  relcnvtr  5148  iotaval  5189  mpteqb  5606  elfvmptrab  5611  chfnrn  5627  elpreima  5635  ffnfv  5674  f1elima  5773  f1eqcocnv  5791  fliftfun  5796  isoresbr  5809  isotr  5816  ovmpodv2  6007  smoiso  6302  nnaordi  6508  nnaword  6511  nnawordi  6515  xpider  6605  iinerm  6606  mptelixpg  6733  dom2lem  6771  nneneq  6856  exmidpw  6907  f1dmvrnfibi  6942  ismkvnex  7152  pr2nelem  7189  exmidfodomrlemeldju  7197  exmidfodomrlemreseldju  7198  netap  7252  2omotaplemap  7255  addcanpig  7332  mulcanpig  7333  enqer  7356  ltexnqi  7407  prarloclemlo  7492  genpcdl  7517  genpcuu  7518  appdivnq  7561  ltprordil  7587  1idprl  7588  1idpru  7589  ltexprlemm  7598  ltexprlemopu  7601  ltexprlemru  7610  cauappcvgprlemladdru  7654  cauappcvgprlemladdrl  7655  caucvgprprlemopu  7697  caucvgsrlemoffcau  7796  caucvgsrlemoffres  7798  ltrenn  7853  axpre-ltadd  7884  addn0nid  8330  apne  8579  aptap  8606  prodgt02  8809  prodge02  8811  mulgt1  8819  divgt0  8828  divge0  8829  cju  8917  nnsub  8957  nominpos  9155  zltnle  9298  nn0n0n1ge2  9322  zdcle  9328  btwnnz  9346  uzm1  9557  supinfneg  9594  infsupneg  9595  ublbneg  9612  cnref1o  9649  ltsubrp  9689  ltaddrp  9690  xnn0dcle  9801  npnflt  9814  nmnfgt  9817  ge0nemnf  9823  xltnegi  9834  xnn0xadd0  9866  iccsupr  9965  icoshft  9989  iccshftri  9994  iccshftli  9996  iccdili  9998  icccntri  10000  fzdcel  10039  fznlem  10040  fzen  10042  fzofzim  10187  eluzgtdifelfzo  10196  elfzonelfzo  10229  qltnle  10245  addmodlteq  10397  qsqeqor  10630  apexp1  10697  fihashf1rn  10767  cjre  10890  caucvgre  10989  icodiamlt  11188  zsumdc  11391  zproddc  11586  reeff1  11707  dvdsmod0  11799  dvds2lem  11809  muldvds1  11822  dvdscmulr  11826  dvdsmulcr  11827  dvdsdivcl  11855  oddnn02np1  11884  ndvdsadd  11935  zeqzmulgcd  11970  bezoutlemmain  11998  dfgcd2  12014  gcdmultiple  12020  coprmdvds  12091  divgcdodd  12142  isprm6  12146  prmdvdsexpr  12149  cncongrprm  12156  phiprmpw  12221  modprm0  12253  pythagtriplem4  12267  pcz  12330  difsqpwdvds  12336  pcadd  12338  1arith  12364  isgrpid2  12912  ringinvnz1ne0  13224  lmss  13716  cnplimcim  14106  dvcn  14134  lgseisenlem2  14421  2sqlem6  14437  ch2var  14489  bj-rspgt  14508  bj-charfundcALT  14531  bj-nntrans  14673  bj-nnelirr  14675  bj-omtrans  14678  setindft  14687  bj-inf2vnlem3  14694  bj-inf2vnlem4  14695  bj-findis  14701  pw1nct  14722