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  680  mtbiri  682  orbi2d  798  pm5.15dc  1434  exlimd2  1644  exintr  1683  19.9d  1709  19.23t  1725  chvarfv  1748  dral1  1779  spimt  1785  cbvalv1  1800  cbvalh  1802  chvar  1806  exdistrfor  1849  sbequi  1888  spv  1909  cbvexvw  1970  eqrdav  2231  cleqh  2332  ceqsalg  2842  vtoclf  2868  vtocl2  2870  vtocl3  2871  spcdv  2902  rspcdv  2924  elabgt  2958  sbcn1  3090  sbcim1  3091  sbcbi1  3092  sbeqalb  3099  sbcel21v  3107  eqrd  3256  rabsnifsb  3757  exmidsssn  4315  exmidsssnc  4316  copsexg  4360  euotd  4371  rexxfrd  4584  relop  4905  reldmm  4975  elres  5074  rnxpid  5197  relcnvtr  5282  iotaval  5324  mpteqb  5768  elfvmptrab  5773  chfnrn  5789  elpreima  5797  ffnfv  5835  f1elima  5946  f1eqcocnv  5964  fliftfun  5969  isoresbr  5982  isotr  5989  ovmpodv2  6187  ressuppss  6454  funsssuppss  6458  smoiso  6533  nnaordi  6741  nnaword  6744  nnawordi  6748  xpider  6840  iinerm  6841  mptelixpg  6969  dom2lem  7011  nneneq  7111  exmidpw  7168  infidc  7201  f1dmvrnfibi  7211  fsuppimp  7245  ismkvnex  7446  pr2nelem  7488  exmidfodomrlemeldju  7502  exmidfodomrlemreseldju  7503  netap  7568  2omotaplemap  7571  addcanpig  7649  mulcanpig  7650  enqer  7673  ltexnqi  7724  prarloclemlo  7809  genpcdl  7834  genpcuu  7835  appdivnq  7878  ltprordil  7904  1idprl  7905  1idpru  7906  ltexprlemm  7915  ltexprlemopu  7918  ltexprlemru  7927  cauappcvgprlemladdru  7971  cauappcvgprlemladdrl  7972  caucvgprprlemopu  8014  caucvgsrlemoffcau  8113  caucvgsrlemoffres  8115  ltrenn  8170  axpre-ltadd  8201  addn0nid  8647  apne  8897  aptap  8924  prodgt02  9127  prodge02  9129  mulgt1  9137  divgt0  9146  divge0  9147  cju  9235  nnsub  9276  nominpos  9476  zltnle  9623  nn0n0n1ge2  9648  zdcle  9654  btwnnz  9672  uzm1  9885  supinfneg  9927  infsupneg  9928  ublbneg  9945  cnref1o  9983  ltsubrp  10023  ltaddrp  10024  xnn0dcle  10135  npnflt  10148  nmnfgt  10151  ge0nemnf  10157  xltnegi  10168  xnn0xadd0  10200  iccsupr  10299  icoshft  10323  iccshftri  10328  iccshftli  10330  iccdili  10332  icccntri  10334  fzdcel  10374  fznlem  10375  fzen  10377  fzofzim  10527  eluzgtdifelfzo  10542  elfzonelfzo  10575  qltnle  10603  addmodlteq  10760  qsqeqor  11012  apexp1  11080  fihashf1rn  11151  lswlgt0cl  11277  ccatalpha  11301  pfxfv  11376  pfxsuff1eqwrdeq  11391  ccatopth2  11409  swrdccat  11427  swrdccat3blem  11431  reuccatpfxs1lem  11438  cjre  11567  caucvgre  11666  icodiamlt  11865  zsumdc  12070  zproddc  12265  reeff1  12386  dvdsmod0  12479  dvds2lem  12489  muldvds1  12502  dvdscmulr  12506  dvdsmulcr  12507  dvdsdivcl  12536  oddnn02np1  12566  ndvdsadd  12617  bitsinv1lem  12647  zeqzmulgcd  12666  bezoutlemmain  12694  dfgcd2  12710  gcdmultiple  12716  coprmdvds  12789  divgcdodd  12840  isprm6  12844  prmdvdsexpr  12847  cncongrprm  12854  phiprmpw  12919  modprm0  12952  pythagtriplem4  12966  pcz  13030  difsqpwdvds  13036  pcadd  13038  1arith  13065  isgrpid2  13753  ghmghmrn  13980  ghmf1  13990  kerf1ghm  13991  imasabl  14053  ringinvnz1ne0  14193  subrngringnsg  14350  domnmuln0  14419  rnglidlmcl  14628  znf1o  14799  znidom  14805  lmss  15111  cnplimcim  15532  dvcn  15565  fsumdvdsmul  15859  gausslemma2dlem1a  15931  lgseisenlem2  15944  lgsquad2  15956  2lgslem1b  15962  2sqlem6  15993  upgrpredgv  16141  upgredgpr  16144  uhgr0v0e  16229  subgrprop  16254  wlkpropg  16319  upgrwlkcompim  16357  uspgr2wlkeq  16360  wlklenvclwlk  16368  wlkres  16374  clwwlk1loop  16394  umgrclwwlkge2  16397  clwwlkn1loopb  16415  clwwlknonex2lem2  16433  ch2var  16539  bj-rspgt  16558  bj-charfundcALT  16579  bj-nntrans  16721  bj-nnelirr  16723  bj-omtrans  16726  setindft  16735  bj-inf2vnlem3  16742  bj-inf2vnlem4  16743  bj-findis  16749  pw1nct  16777