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  674  mtbiri  676  orbi2d  791  pm5.15dc  1408  exlimd2  1617  exintr  1656  19.9d  1683  19.23t  1699  chvarfv  1722  dral1  1752  spimt  1758  cbvalv1  1773  cbvalh  1775  chvar  1779  exdistrfor  1822  sbequi  1861  spv  1882  cbvexvw  1943  eqrdav  2203  cleqh  2304  ceqsalg  2799  vtoclf  2825  vtocl2  2827  vtocl3  2828  spcdv  2857  rspcdv  2879  elabgt  2913  sbcn1  3045  sbcim1  3046  sbcbi1  3047  sbeqalb  3054  sbcel21v  3062  eqrd  3210  exmidsssn  4245  exmidsssnc  4246  copsexg  4287  euotd  4297  rexxfrd  4508  relop  4826  elres  4992  rnxpid  5114  relcnvtr  5199  iotaval  5240  mpteqb  5664  elfvmptrab  5669  chfnrn  5685  elpreima  5693  ffnfv  5732  f1elima  5832  f1eqcocnv  5850  fliftfun  5855  isoresbr  5868  isotr  5875  ovmpodv2  6069  smoiso  6378  nnaordi  6584  nnaword  6587  nnawordi  6591  xpider  6683  iinerm  6684  mptelixpg  6811  dom2lem  6849  nneneq  6936  exmidpw  6987  infidc  7018  f1dmvrnfibi  7028  ismkvnex  7239  pr2nelem  7281  exmidfodomrlemeldju  7289  exmidfodomrlemreseldju  7290  netap  7348  2omotaplemap  7351  addcanpig  7429  mulcanpig  7430  enqer  7453  ltexnqi  7504  prarloclemlo  7589  genpcdl  7614  genpcuu  7615  appdivnq  7658  ltprordil  7684  1idprl  7685  1idpru  7686  ltexprlemm  7695  ltexprlemopu  7698  ltexprlemru  7707  cauappcvgprlemladdru  7751  cauappcvgprlemladdrl  7752  caucvgprprlemopu  7794  caucvgsrlemoffcau  7893  caucvgsrlemoffres  7895  ltrenn  7950  axpre-ltadd  7981  addn0nid  8428  apne  8678  aptap  8705  prodgt02  8908  prodge02  8910  mulgt1  8918  divgt0  8927  divge0  8928  cju  9016  nnsub  9057  nominpos  9257  zltnle  9400  nn0n0n1ge2  9425  zdcle  9431  btwnnz  9449  uzm1  9661  supinfneg  9698  infsupneg  9699  ublbneg  9716  cnref1o  9754  ltsubrp  9794  ltaddrp  9795  xnn0dcle  9906  npnflt  9919  nmnfgt  9922  ge0nemnf  9928  xltnegi  9939  xnn0xadd0  9971  iccsupr  10070  icoshft  10094  iccshftri  10099  iccshftli  10101  iccdili  10103  icccntri  10105  fzdcel  10144  fznlem  10145  fzen  10147  fzofzim  10293  eluzgtdifelfzo  10307  elfzonelfzo  10340  qltnle  10367  addmodlteq  10524  qsqeqor  10776  apexp1  10844  fihashf1rn  10914  lswlgt0cl  11020  cjre  11112  caucvgre  11211  icodiamlt  11410  zsumdc  11614  zproddc  11809  reeff1  11930  dvdsmod0  12023  dvds2lem  12033  muldvds1  12046  dvdscmulr  12050  dvdsmulcr  12051  dvdsdivcl  12080  oddnn02np1  12110  ndvdsadd  12161  bitsinv1lem  12191  zeqzmulgcd  12210  bezoutlemmain  12238  dfgcd2  12254  gcdmultiple  12260  coprmdvds  12333  divgcdodd  12384  isprm6  12388  prmdvdsexpr  12391  cncongrprm  12398  phiprmpw  12463  modprm0  12496  pythagtriplem4  12510  pcz  12574  difsqpwdvds  12580  pcadd  12582  1arith  12609  isgrpid2  13290  ghmghmrn  13517  ghmf1  13527  kerf1ghm  13528  imasabl  13590  ringinvnz1ne0  13729  subrngringnsg  13885  domnmuln0  13953  rnglidlmcl  14160  znf1o  14331  znidom  14337  lmss  14636  cnplimcim  15057  dvcn  15090  fsumdvdsmul  15381  gausslemma2dlem1a  15453  lgseisenlem2  15466  lgsquad2  15478  2lgslem1b  15484  2sqlem6  15515  ch2var  15567  bj-rspgt  15586  bj-charfundcALT  15609  bj-nntrans  15751  bj-nnelirr  15753  bj-omtrans  15756  setindft  15765  bj-inf2vnlem3  15772  bj-inf2vnlem4  15773  bj-findis  15779  pw1nct  15804