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  679  mtbiri  681  orbi2d  797  pm5.15dc  1433  exlimd2  1643  exintr  1682  19.9d  1709  19.23t  1725  chvarfv  1748  dral1  1778  spimt  1784  cbvalv1  1799  cbvalh  1801  chvar  1805  exdistrfor  1848  sbequi  1887  spv  1908  cbvexvw  1969  eqrdav  2230  cleqh  2331  ceqsalg  2831  vtoclf  2857  vtocl2  2859  vtocl3  2860  spcdv  2891  rspcdv  2913  elabgt  2947  sbcn1  3079  sbcim1  3080  sbcbi1  3081  sbeqalb  3088  sbcel21v  3096  eqrd  3245  rabsnifsb  3737  exmidsssn  4292  exmidsssnc  4293  copsexg  4336  euotd  4347  rexxfrd  4560  relop  4880  reldmm  4950  elres  5049  rnxpid  5171  relcnvtr  5256  iotaval  5298  mpteqb  5737  elfvmptrab  5742  chfnrn  5758  elpreima  5766  ffnfv  5805  f1elima  5913  f1eqcocnv  5931  fliftfun  5936  isoresbr  5949  isotr  5956  ovmpodv2  6154  smoiso  6467  nnaordi  6675  nnaword  6678  nnawordi  6682  xpider  6774  iinerm  6775  mptelixpg  6902  dom2lem  6944  nneneq  7042  exmidpw  7099  infidc  7132  f1dmvrnfibi  7142  ismkvnex  7353  pr2nelem  7395  exmidfodomrlemeldju  7409  exmidfodomrlemreseldju  7410  netap  7472  2omotaplemap  7475  addcanpig  7553  mulcanpig  7554  enqer  7577  ltexnqi  7628  prarloclemlo  7713  genpcdl  7738  genpcuu  7739  appdivnq  7782  ltprordil  7808  1idprl  7809  1idpru  7810  ltexprlemm  7819  ltexprlemopu  7822  ltexprlemru  7831  cauappcvgprlemladdru  7875  cauappcvgprlemladdrl  7876  caucvgprprlemopu  7918  caucvgsrlemoffcau  8017  caucvgsrlemoffres  8019  ltrenn  8074  axpre-ltadd  8105  addn0nid  8552  apne  8802  aptap  8829  prodgt02  9032  prodge02  9034  mulgt1  9042  divgt0  9051  divge0  9052  cju  9140  nnsub  9181  nominpos  9381  zltnle  9524  nn0n0n1ge2  9549  zdcle  9555  btwnnz  9573  uzm1  9786  supinfneg  9828  infsupneg  9829  ublbneg  9846  cnref1o  9884  ltsubrp  9924  ltaddrp  9925  xnn0dcle  10036  npnflt  10049  nmnfgt  10052  ge0nemnf  10058  xltnegi  10069  xnn0xadd0  10101  iccsupr  10200  icoshft  10224  iccshftri  10229  iccshftli  10231  iccdili  10233  icccntri  10235  fzdcel  10274  fznlem  10275  fzen  10277  fzofzim  10426  eluzgtdifelfzo  10441  elfzonelfzo  10474  qltnle  10502  addmodlteq  10659  qsqeqor  10911  apexp1  10979  fihashf1rn  11049  lswlgt0cl  11165  ccatalpha  11189  pfxfv  11264  pfxsuff1eqwrdeq  11279  ccatopth2  11297  swrdccat  11315  swrdccat3blem  11319  reuccatpfxs1lem  11326  cjre  11442  caucvgre  11541  icodiamlt  11740  zsumdc  11944  zproddc  12139  reeff1  12260  dvdsmod0  12353  dvds2lem  12363  muldvds1  12376  dvdscmulr  12380  dvdsmulcr  12381  dvdsdivcl  12410  oddnn02np1  12440  ndvdsadd  12491  bitsinv1lem  12521  zeqzmulgcd  12540  bezoutlemmain  12568  dfgcd2  12584  gcdmultiple  12590  coprmdvds  12663  divgcdodd  12714  isprm6  12718  prmdvdsexpr  12721  cncongrprm  12728  phiprmpw  12793  modprm0  12826  pythagtriplem4  12840  pcz  12904  difsqpwdvds  12910  pcadd  12912  1arith  12939  isgrpid2  13622  ghmghmrn  13849  ghmf1  13859  kerf1ghm  13860  imasabl  13922  ringinvnz1ne0  14061  subrngringnsg  14218  domnmuln0  14286  rnglidlmcl  14493  znf1o  14664  znidom  14670  lmss  14969  cnplimcim  15390  dvcn  15423  fsumdvdsmul  15714  gausslemma2dlem1a  15786  lgseisenlem2  15799  lgsquad2  15811  2lgslem1b  15817  2sqlem6  15848  upgrpredgv  15996  upgredgpr  15999  uhgr0v0e  16084  subgrprop  16109  wlkpropg  16174  upgrwlkcompim  16212  uspgr2wlkeq  16215  wlklenvclwlk  16223  wlkres  16229  clwwlk1loop  16249  umgrclwwlkge2  16252  clwwlkn1loopb  16270  clwwlknonex2lem2  16288  ch2var  16363  bj-rspgt  16382  bj-charfundcALT  16404  bj-nntrans  16546  bj-nnelirr  16548  bj-omtrans  16551  setindft  16560  bj-inf2vnlem3  16567  bj-inf2vnlem4  16568  bj-findis  16574  pw1nct  16604