Theorem biimpd 144

Description: Deduce an implication from a logical equivalence. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
biimpd.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
biimpd	⊢ (𝜑 → (𝜓 → 𝜒))

Proof of Theorem biimpd

Step	Hyp	Ref	Expression
1		biimpd.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		biimp 118	. 2 ⊢ ((𝜓 ↔ 𝜒) → (𝜓 → 𝜒))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝜓 → 𝜒))

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  677  mtbiri  679  orbi2d  795  pm5.15dc  1431  exlimd2  1641  exintr  1680  19.9d  1707  19.23t  1723  chvarfv  1746  dral1  1776  spimt  1782  cbvalv1  1797  cbvalh  1799  chvar  1803  exdistrfor  1846  sbequi  1885  spv  1906  cbvexvw  1967  eqrdav  2228  cleqh  2329  ceqsalg  2829  vtoclf  2855  vtocl2  2857  vtocl3  2858  spcdv  2889  rspcdv  2911  elabgt  2945  sbcn1  3077  sbcim1  3078  sbcbi1  3079  sbeqalb  3086  sbcel21v  3094  eqrd  3243  rabsnifsb  3735  exmidsssn  4290  exmidsssnc  4291  copsexg  4334  euotd  4345  rexxfrd  4558  relop  4878  reldmm  4948  elres  5047  rnxpid  5169  relcnvtr  5254  iotaval  5296  mpteqb  5733  elfvmptrab  5738  chfnrn  5754  elpreima  5762  ffnfv  5801  f1elima  5909  f1eqcocnv  5927  fliftfun  5932  isoresbr  5945  isotr  5952  ovmpodv2  6150  smoiso  6463  nnaordi  6671  nnaword  6674  nnawordi  6678  xpider  6770  iinerm  6771  mptelixpg  6898  dom2lem  6940  nneneq  7038  exmidpw  7093  infidc  7124  f1dmvrnfibi  7134  ismkvnex  7345  pr2nelem  7387  exmidfodomrlemeldju  7400  exmidfodomrlemreseldju  7401  netap  7463  2omotaplemap  7466  addcanpig  7544  mulcanpig  7545  enqer  7568  ltexnqi  7619  prarloclemlo  7704  genpcdl  7729  genpcuu  7730  appdivnq  7773  ltprordil  7799  1idprl  7800  1idpru  7801  ltexprlemm  7810  ltexprlemopu  7813  ltexprlemru  7822  cauappcvgprlemladdru  7866  cauappcvgprlemladdrl  7867  caucvgprprlemopu  7909  caucvgsrlemoffcau  8008  caucvgsrlemoffres  8010  ltrenn  8065  axpre-ltadd  8096  addn0nid  8543  apne  8793  aptap  8820  prodgt02  9023  prodge02  9025  mulgt1  9033  divgt0  9042  divge0  9043  cju  9131  nnsub  9172  nominpos  9372  zltnle  9515  nn0n0n1ge2  9540  zdcle  9546  btwnnz  9564  uzm1  9777  supinfneg  9819  infsupneg  9820  ublbneg  9837  cnref1o  9875  ltsubrp  9915  ltaddrp  9916  xnn0dcle  10027  npnflt  10040  nmnfgt  10043  ge0nemnf  10049  xltnegi  10060  xnn0xadd0  10092  iccsupr  10191  icoshft  10215  iccshftri  10220  iccshftli  10222  iccdili  10224  icccntri  10226  fzdcel  10265  fznlem  10266  fzen  10268  fzofzim  10417  eluzgtdifelfzo  10432  elfzonelfzo  10465  qltnle  10493  addmodlteq  10650  qsqeqor  10902  apexp1  10970  fihashf1rn  11040  lswlgt0cl  11156  ccatalpha  11180  pfxfv  11255  pfxsuff1eqwrdeq  11270  ccatopth2  11288  swrdccat  11306  swrdccat3blem  11310  reuccatpfxs1lem  11317  cjre  11433  caucvgre  11532  icodiamlt  11731  zsumdc  11935  zproddc  12130  reeff1  12251  dvdsmod0  12344  dvds2lem  12354  muldvds1  12367  dvdscmulr  12371  dvdsmulcr  12372  dvdsdivcl  12401  oddnn02np1  12431  ndvdsadd  12482  bitsinv1lem  12512  zeqzmulgcd  12531  bezoutlemmain  12559  dfgcd2  12575  gcdmultiple  12581  coprmdvds  12654  divgcdodd  12705  isprm6  12709  prmdvdsexpr  12712  cncongrprm  12719  phiprmpw  12784  modprm0  12817  pythagtriplem4  12831  pcz  12895  difsqpwdvds  12901  pcadd  12903  1arith  12930  isgrpid2  13613  ghmghmrn  13840  ghmf1  13850  kerf1ghm  13851  imasabl  13913  ringinvnz1ne0  14052  subrngringnsg  14209  domnmuln0  14277  rnglidlmcl  14484  znf1o  14655  znidom  14661  lmss  14960  cnplimcim  15381  dvcn  15414  fsumdvdsmul  15705  gausslemma2dlem1a  15777  lgseisenlem2  15790  lgsquad2  15802  2lgslem1b  15808  2sqlem6  15839  upgrpredgv  15985  upgredgpr  15988  uhgr0v0e  16073  wlkpropg  16121  upgrwlkcompim  16159  uspgr2wlkeq  16162  wlklenvclwlk  16170  wlkres  16174  clwwlk1loop  16194  umgrclwwlkge2  16197  clwwlkn1loopb  16215  clwwlknonex2lem2  16233  ch2var  16299  bj-rspgt  16318  bj-charfundcALT  16340  bj-nntrans  16482  bj-nnelirr  16484  bj-omtrans  16487  setindft  16496  bj-inf2vnlem3  16503  bj-inf2vnlem4  16504  bj-findis  16510  pw1nct  16540