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  1400  exlimd2  1609  exintr  1648  19.9d  1675  19.23t  1691  chvarfv  1714  dral1  1744  spimt  1750  cbvalv1  1765  cbvalh  1767  chvar  1771  exdistrfor  1814  sbequi  1853  spv  1874  cbvexvw  1935  eqrdav  2195  cleqh  2296  ceqsalg  2791  vtoclf  2817  vtocl2  2819  vtocl3  2820  spcdv  2849  rspcdv  2871  elabgt  2905  sbcn1  3037  sbcim1  3038  sbcbi1  3039  sbeqalb  3046  sbcel21v  3054  eqrd  3202  exmidsssn  4236  exmidsssnc  4237  copsexg  4278  euotd  4288  rexxfrd  4499  relop  4817  elres  4983  rnxpid  5105  relcnvtr  5190  iotaval  5231  mpteqb  5655  elfvmptrab  5660  chfnrn  5676  elpreima  5684  ffnfv  5723  f1elima  5823  f1eqcocnv  5841  fliftfun  5846  isoresbr  5859  isotr  5866  ovmpodv2  6060  smoiso  6369  nnaordi  6575  nnaword  6578  nnawordi  6582  xpider  6674  iinerm  6675  mptelixpg  6802  dom2lem  6840  nneneq  6927  exmidpw  6978  infidc  7009  f1dmvrnfibi  7019  ismkvnex  7230  pr2nelem  7272  exmidfodomrlemeldju  7280  exmidfodomrlemreseldju  7281  netap  7339  2omotaplemap  7342  addcanpig  7420  mulcanpig  7421  enqer  7444  ltexnqi  7495  prarloclemlo  7580  genpcdl  7605  genpcuu  7606  appdivnq  7649  ltprordil  7675  1idprl  7676  1idpru  7677  ltexprlemm  7686  ltexprlemopu  7689  ltexprlemru  7698  cauappcvgprlemladdru  7742  cauappcvgprlemladdrl  7743  caucvgprprlemopu  7785  caucvgsrlemoffcau  7884  caucvgsrlemoffres  7886  ltrenn  7941  axpre-ltadd  7972  addn0nid  8419  apne  8669  aptap  8696  prodgt02  8899  prodge02  8901  mulgt1  8909  divgt0  8918  divge0  8919  cju  9007  nnsub  9048  nominpos  9248  zltnle  9391  nn0n0n1ge2  9415  zdcle  9421  btwnnz  9439  uzm1  9651  supinfneg  9688  infsupneg  9689  ublbneg  9706  cnref1o  9744  ltsubrp  9784  ltaddrp  9785  xnn0dcle  9896  npnflt  9909  nmnfgt  9912  ge0nemnf  9918  xltnegi  9929  xnn0xadd0  9961  iccsupr  10060  icoshft  10084  iccshftri  10089  iccshftli  10091  iccdili  10093  icccntri  10095  fzdcel  10134  fznlem  10135  fzen  10137  fzofzim  10283  eluzgtdifelfzo  10292  elfzonelfzo  10325  qltnle  10352  addmodlteq  10509  qsqeqor  10761  apexp1  10829  fihashf1rn  10899  cjre  11066  caucvgre  11165  icodiamlt  11364  zsumdc  11568  zproddc  11763  reeff1  11884  dvdsmod0  11977  dvds2lem  11987  muldvds1  12000  dvdscmulr  12004  dvdsmulcr  12005  dvdsdivcl  12034  oddnn02np1  12064  ndvdsadd  12115  bitsinv1lem  12145  zeqzmulgcd  12164  bezoutlemmain  12192  dfgcd2  12208  gcdmultiple  12214  coprmdvds  12287  divgcdodd  12338  isprm6  12342  prmdvdsexpr  12345  cncongrprm  12352  phiprmpw  12417  modprm0  12450  pythagtriplem4  12464  pcz  12528  difsqpwdvds  12534  pcadd  12536  1arith  12563  isgrpid2  13244  ghmghmrn  13471  ghmf1  13481  kerf1ghm  13482  imasabl  13544  ringinvnz1ne0  13683  subrngringnsg  13839  domnmuln0  13907  rnglidlmcl  14114  znf1o  14285  znidom  14291  lmss  14590  cnplimcim  15011  dvcn  15044  fsumdvdsmul  15335  gausslemma2dlem1a  15407  lgseisenlem2  15420  lgsquad2  15432  2lgslem1b  15438  2sqlem6  15469  ch2var  15521  bj-rspgt  15540  bj-charfundcALT  15563  bj-nntrans  15705  bj-nnelirr  15707  bj-omtrans  15710  setindft  15719  bj-inf2vnlem3  15726  bj-inf2vnlem4  15727  bj-findis  15733  pw1nct  15758