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  675  mtbiri  677  orbi2d  792  pm5.15dc  1409  exlimd2  1619  exintr  1658  19.9d  1685  19.23t  1701  chvarfv  1724  dral1  1754  spimt  1760  cbvalv1  1775  cbvalh  1777  chvar  1781  exdistrfor  1824  sbequi  1863  spv  1884  cbvexvw  1945  eqrdav  2205  cleqh  2306  ceqsalg  2802  vtoclf  2828  vtocl2  2830  vtocl3  2831  spcdv  2862  rspcdv  2884  elabgt  2918  sbcn1  3050  sbcim1  3051  sbcbi1  3052  sbeqalb  3059  sbcel21v  3067  eqrd  3215  exmidsssn  4254  exmidsssnc  4255  copsexg  4296  euotd  4307  rexxfrd  4518  relop  4836  elres  5004  rnxpid  5126  relcnvtr  5211  iotaval  5252  mpteqb  5683  elfvmptrab  5688  chfnrn  5704  elpreima  5712  ffnfv  5751  f1elima  5855  f1eqcocnv  5873  fliftfun  5878  isoresbr  5891  isotr  5898  ovmpodv2  6092  smoiso  6401  nnaordi  6607  nnaword  6610  nnawordi  6614  xpider  6706  iinerm  6707  mptelixpg  6834  dom2lem  6876  nneneq  6969  exmidpw  7020  infidc  7051  f1dmvrnfibi  7061  ismkvnex  7272  pr2nelem  7314  exmidfodomrlemeldju  7323  exmidfodomrlemreseldju  7324  netap  7386  2omotaplemap  7389  addcanpig  7467  mulcanpig  7468  enqer  7491  ltexnqi  7542  prarloclemlo  7627  genpcdl  7652  genpcuu  7653  appdivnq  7696  ltprordil  7722  1idprl  7723  1idpru  7724  ltexprlemm  7733  ltexprlemopu  7736  ltexprlemru  7745  cauappcvgprlemladdru  7789  cauappcvgprlemladdrl  7790  caucvgprprlemopu  7832  caucvgsrlemoffcau  7931  caucvgsrlemoffres  7933  ltrenn  7988  axpre-ltadd  8019  addn0nid  8466  apne  8716  aptap  8743  prodgt02  8946  prodge02  8948  mulgt1  8956  divgt0  8965  divge0  8966  cju  9054  nnsub  9095  nominpos  9295  zltnle  9438  nn0n0n1ge2  9463  zdcle  9469  btwnnz  9487  uzm1  9699  supinfneg  9736  infsupneg  9737  ublbneg  9754  cnref1o  9792  ltsubrp  9832  ltaddrp  9833  xnn0dcle  9944  npnflt  9957  nmnfgt  9960  ge0nemnf  9966  xltnegi  9977  xnn0xadd0  10009  iccsupr  10108  icoshft  10132  iccshftri  10137  iccshftli  10139  iccdili  10141  icccntri  10143  fzdcel  10182  fznlem  10183  fzen  10185  fzofzim  10334  eluzgtdifelfzo  10348  elfzonelfzo  10381  qltnle  10408  addmodlteq  10565  qsqeqor  10817  apexp1  10885  fihashf1rn  10955  lswlgt0cl  11068  pfxfv  11160  pfxsuff1eqwrdeq  11175  ccatopth2  11193  cjre  11268  caucvgre  11367  icodiamlt  11566  zsumdc  11770  zproddc  11965  reeff1  12086  dvdsmod0  12179  dvds2lem  12189  muldvds1  12202  dvdscmulr  12206  dvdsmulcr  12207  dvdsdivcl  12236  oddnn02np1  12266  ndvdsadd  12317  bitsinv1lem  12347  zeqzmulgcd  12366  bezoutlemmain  12394  dfgcd2  12410  gcdmultiple  12416  coprmdvds  12489  divgcdodd  12540  isprm6  12544  prmdvdsexpr  12547  cncongrprm  12554  phiprmpw  12619  modprm0  12652  pythagtriplem4  12666  pcz  12730  difsqpwdvds  12736  pcadd  12738  1arith  12765  isgrpid2  13447  ghmghmrn  13674  ghmf1  13684  kerf1ghm  13685  imasabl  13747  ringinvnz1ne0  13886  subrngringnsg  14042  domnmuln0  14110  rnglidlmcl  14317  znf1o  14488  znidom  14494  lmss  14793  cnplimcim  15214  dvcn  15247  fsumdvdsmul  15538  gausslemma2dlem1a  15610  lgseisenlem2  15623  lgsquad2  15635  2lgslem1b  15641  2sqlem6  15672  ch2var  15842  bj-rspgt  15861  bj-charfundcALT  15883  bj-nntrans  16025  bj-nnelirr  16027  bj-omtrans  16030  setindft  16039  bj-inf2vnlem3  16046  bj-inf2vnlem4  16047  bj-findis  16053  pw1nct  16081