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  8329  apne  8578  aptap  8605  prodgt02  8808  prodge02  8810  mulgt1  8818  divgt0  8827  divge0  8828  cju  8916  nnsub  8956  nominpos  9154  zltnle  9297  nn0n0n1ge2  9321  zdcle  9327  btwnnz  9345  uzm1  9556  supinfneg  9593  infsupneg  9594  ublbneg  9611  cnref1o  9648  ltsubrp  9688  ltaddrp  9689  xnn0dcle  9800  npnflt  9813  nmnfgt  9816  ge0nemnf  9822  xltnegi  9833  xnn0xadd0  9865  iccsupr  9964  icoshft  9988  iccshftri  9993  iccshftli  9995  iccdili  9997  icccntri  9999  fzdcel  10037  fznlem  10038  fzen  10040  fzofzim  10185  eluzgtdifelfzo  10194  elfzonelfzo  10227  qltnle  10243  addmodlteq  10395  qsqeqor  10627  apexp1  10693  fihashf1rn  10763  cjre  10886  caucvgre  10985  icodiamlt  11184  zsumdc  11387  zproddc  11582  reeff1  11703  dvdsmod0  11795  dvds2lem  11805  muldvds1  11818  dvdscmulr  11822  dvdsmulcr  11823  dvdsdivcl  11850  oddnn02np1  11879  ndvdsadd  11930  zeqzmulgcd  11965  bezoutlemmain  11993  dfgcd2  12009  gcdmultiple  12015  coprmdvds  12086  divgcdodd  12137  isprm6  12141  prmdvdsexpr  12144  cncongrprm  12151  phiprmpw  12216  modprm0  12248  pythagtriplem4  12262  pcz  12325  difsqpwdvds  12331  pcadd  12333  1arith  12359  isgrpid2  12907  ringinvnz1ne0  13219  lmss  13677  cnplimcim  14067  dvcn  14095  2sqlem6  14387  ch2var  14439  bj-rspgt  14458  bj-charfundcALT  14481  bj-nntrans  14623  bj-nnelirr  14625  bj-omtrans  14628  setindft  14637  bj-inf2vnlem3  14644  bj-inf2vnlem4  14645  bj-findis  14651  pw1nct  14672