Theorem biimpd 143

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		bi1 117	. 2 |- ( ( ps <-> ch ) -> ( ps -> ch ) )
3	1, 2	syl 14	1 |- ( ph -> ( ps -> ch ) )

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpbid  146  sylibd  148  sylbid  149  mpbidi  150  syl5ib  153  syl6bi  162  ibi  175  imbi1d  230  biimpa  294  mtbird  663  mtbiri  665  orbi2d  780  pm5.15dc  1368  exlimd2  1575  exintr  1614  19.9d  1640  19.23t  1656  dral1  1709  spimt  1715  cbvalh  1727  chvar  1731  exdistrfor  1773  sbequi  1812  spv  1833  eqrdav  2139  cleqh  2240  ceqsalg  2717  vtoclf  2742  vtocl2  2744  vtocl3  2745  spcdv  2774  rspcdv  2796  elabgt  2829  sbcn1  2960  sbcim1  2961  sbcbi1  2962  sbeqalb  2969  sbcel21v  2977  eqrd  3120  exmidsssn  4133  exmidsssnc  4134  copsexg  4174  euotd  4184  rexxfrd  4392  relop  4697  elres  4863  rnxpid  4981  relcnvtr  5066  iotaval  5107  mpteqb  5519  elfvmptrab  5524  chfnrn  5539  elpreima  5547  ffnfv  5586  f1elima  5682  f1eqcocnv  5700  fliftfun  5705  isoresbr  5718  isotr  5725  ovmpodv2  5912  smoiso  6207  nnaordi  6412  nnaword  6415  nnawordi  6419  xpider  6508  iinerm  6509  mptelixpg  6636  dom2lem  6674  nneneq  6759  exmidpw  6810  f1dmvrnfibi  6840  ismkvnex  7037  pr2nelem  7064  exmidfodomrlemeldju  7072  exmidfodomrlemreseldju  7073  addcanpig  7166  mulcanpig  7167  enqer  7190  ltexnqi  7241  prarloclemlo  7326  genpcdl  7351  genpcuu  7352  appdivnq  7395  ltprordil  7421  1idprl  7422  1idpru  7423  ltexprlemm  7432  ltexprlemopu  7435  ltexprlemru  7444  cauappcvgprlemladdru  7488  cauappcvgprlemladdrl  7489  caucvgprprlemopu  7531  caucvgsrlemoffcau  7630  caucvgsrlemoffres  7632  ltrenn  7687  axpre-ltadd  7718  addn0nid  8160  apne  8409  prodgt02  8635  prodge02  8637  mulgt1  8645  divgt0  8654  divge0  8655  cju  8743  nnsub  8783  nominpos  8981  zltnle  9124  nn0n0n1ge2  9145  zdcle  9151  btwnnz  9169  uzm1  9380  supinfneg  9417  infsupneg  9418  ublbneg  9432  cnref1o  9469  ltsubrp  9507  ltaddrp  9508  npnflt  9628  nmnfgt  9631  ge0nemnf  9637  xltnegi  9648  xnn0xadd0  9680  iccsupr  9779  icoshft  9803  iccshftri  9808  iccshftli  9810  iccdili  9812  icccntri  9814  fzdcel  9851  fznlem  9852  fzen  9854  fzofzim  9996  eluzgtdifelfzo  10005  elfzonelfzo  10038  qltnle  10054  addmodlteq  10202  apexp1  10496  fihashf1rn  10567  cjre  10686  caucvgre  10785  icodiamlt  10984  zsumdc  11185  zproddc  11380  reeff1  11443  dvds2lem  11541  muldvds1  11554  dvdscmulr  11558  dvdsmulcr  11559  dvdsdivcl  11584  oddnn02np1  11613  ndvdsadd  11664  zeqzmulgcd  11695  bezoutlemmain  11722  dfgcd2  11738  gcdmultiple  11744  coprmdvds  11809  divgcdodd  11857  isprm6  11861  prmdvdsexpr  11864  cncongrprm  11871  phiprmpw  11934  lmss  12454  cnplimcim  12844  dvcn  12872  ch2var  13145  bj-rspgt  13164  bj-nntrans  13320  bj-nnelirr  13322  bj-omtrans  13325  setindft  13334  bj-inf2vnlem3  13341  bj-inf2vnlem4  13342  bj-findis  13348  pw1nct  13371