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  2828  vtoclf  2854  vtocl2  2856  vtocl3  2857  spcdv  2888  rspcdv  2910  elabgt  2944  sbcn1  3076  sbcim1  3077  sbcbi1  3078  sbeqalb  3085  sbcel21v  3093  eqrd  3242  exmidsssn  4285  exmidsssnc  4286  copsexg  4329  euotd  4340  rexxfrd  4553  relop  4871  reldmm  4941  elres  5040  rnxpid  5162  relcnvtr  5247  iotaval  5289  mpteqb  5724  elfvmptrab  5729  chfnrn  5745  elpreima  5753  ffnfv  5792  f1elima  5896  f1eqcocnv  5914  fliftfun  5919  isoresbr  5932  isotr  5939  ovmpodv2  6137  smoiso  6446  nnaordi  6652  nnaword  6655  nnawordi  6659  xpider  6751  iinerm  6752  mptelixpg  6879  dom2lem  6921  nneneq  7014  exmidpw  7066  infidc  7097  f1dmvrnfibi  7107  ismkvnex  7318  pr2nelem  7360  exmidfodomrlemeldju  7373  exmidfodomrlemreseldju  7374  netap  7436  2omotaplemap  7439  addcanpig  7517  mulcanpig  7518  enqer  7541  ltexnqi  7592  prarloclemlo  7677  genpcdl  7702  genpcuu  7703  appdivnq  7746  ltprordil  7772  1idprl  7773  1idpru  7774  ltexprlemm  7783  ltexprlemopu  7786  ltexprlemru  7795  cauappcvgprlemladdru  7839  cauappcvgprlemladdrl  7840  caucvgprprlemopu  7882  caucvgsrlemoffcau  7981  caucvgsrlemoffres  7983  ltrenn  8038  axpre-ltadd  8069  addn0nid  8516  apne  8766  aptap  8793  prodgt02  8996  prodge02  8998  mulgt1  9006  divgt0  9015  divge0  9016  cju  9104  nnsub  9145  nominpos  9345  zltnle  9488  nn0n0n1ge2  9513  zdcle  9519  btwnnz  9537  uzm1  9749  supinfneg  9786  infsupneg  9787  ublbneg  9804  cnref1o  9842  ltsubrp  9882  ltaddrp  9883  xnn0dcle  9994  npnflt  10007  nmnfgt  10010  ge0nemnf  10016  xltnegi  10027  xnn0xadd0  10059  iccsupr  10158  icoshft  10182  iccshftri  10187  iccshftli  10189  iccdili  10191  icccntri  10193  fzdcel  10232  fznlem  10233  fzen  10235  fzofzim  10384  eluzgtdifelfzo  10398  elfzonelfzo  10431  qltnle  10458  addmodlteq  10615  qsqeqor  10867  apexp1  10935  fihashf1rn  11005  lswlgt0cl  11119  pfxfv  11211  pfxsuff1eqwrdeq  11226  ccatopth2  11244  swrdccat  11262  swrdccat3blem  11266  reuccatpfxs1lem  11273  cjre  11388  caucvgre  11487  icodiamlt  11686  zsumdc  11890  zproddc  12085  reeff1  12206  dvdsmod0  12299  dvds2lem  12309  muldvds1  12322  dvdscmulr  12326  dvdsmulcr  12327  dvdsdivcl  12356  oddnn02np1  12386  ndvdsadd  12437  bitsinv1lem  12467  zeqzmulgcd  12486  bezoutlemmain  12514  dfgcd2  12530  gcdmultiple  12536  coprmdvds  12609  divgcdodd  12660  isprm6  12664  prmdvdsexpr  12667  cncongrprm  12674  phiprmpw  12739  modprm0  12772  pythagtriplem4  12786  pcz  12850  difsqpwdvds  12856  pcadd  12858  1arith  12885  isgrpid2  13568  ghmghmrn  13795  ghmf1  13805  kerf1ghm  13806  imasabl  13868  ringinvnz1ne0  14007  subrngringnsg  14163  domnmuln0  14231  rnglidlmcl  14438  znf1o  14609  znidom  14615  lmss  14914  cnplimcim  15335  dvcn  15368  fsumdvdsmul  15659  gausslemma2dlem1a  15731  lgseisenlem2  15744  lgsquad2  15756  2lgslem1b  15762  2sqlem6  15793  upgrpredgv  15938  upgredgpr  15941  wlkpropg  16030  ch2var  16089  bj-rspgt  16108  bj-charfundcALT  16130  bj-nntrans  16272  bj-nnelirr  16274  bj-omtrans  16277  setindft  16286  bj-inf2vnlem3  16293  bj-inf2vnlem4  16294  bj-findis  16300  pw1nct  16328