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  4286  exmidsssnc  4287  copsexg  4330  euotd  4341  rexxfrd  4554  relop  4872  reldmm  4942  elres  5041  rnxpid  5163  relcnvtr  5248  iotaval  5290  mpteqb  5727  elfvmptrab  5732  chfnrn  5748  elpreima  5756  ffnfv  5795  f1elima  5903  f1eqcocnv  5921  fliftfun  5926  isoresbr  5939  isotr  5946  ovmpodv2  6144  smoiso  6454  nnaordi  6662  nnaword  6665  nnawordi  6669  xpider  6761  iinerm  6762  mptelixpg  6889  dom2lem  6931  nneneq  7026  exmidpw  7081  infidc  7112  f1dmvrnfibi  7122  ismkvnex  7333  pr2nelem  7375  exmidfodomrlemeldju  7388  exmidfodomrlemreseldju  7389  netap  7451  2omotaplemap  7454  addcanpig  7532  mulcanpig  7533  enqer  7556  ltexnqi  7607  prarloclemlo  7692  genpcdl  7717  genpcuu  7718  appdivnq  7761  ltprordil  7787  1idprl  7788  1idpru  7789  ltexprlemm  7798  ltexprlemopu  7801  ltexprlemru  7810  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  caucvgprprlemopu  7897  caucvgsrlemoffcau  7996  caucvgsrlemoffres  7998  ltrenn  8053  axpre-ltadd  8084  addn0nid  8531  apne  8781  aptap  8808  prodgt02  9011  prodge02  9013  mulgt1  9021  divgt0  9030  divge0  9031  cju  9119  nnsub  9160  nominpos  9360  zltnle  9503  nn0n0n1ge2  9528  zdcle  9534  btwnnz  9552  uzm1  9765  supinfneg  9802  infsupneg  9803  ublbneg  9820  cnref1o  9858  ltsubrp  9898  ltaddrp  9899  xnn0dcle  10010  npnflt  10023  nmnfgt  10026  ge0nemnf  10032  xltnegi  10043  xnn0xadd0  10075  iccsupr  10174  icoshft  10198  iccshftri  10203  iccshftli  10205  iccdili  10207  icccntri  10209  fzdcel  10248  fznlem  10249  fzen  10251  fzofzim  10400  eluzgtdifelfzo  10415  elfzonelfzo  10448  qltnle  10475  addmodlteq  10632  qsqeqor  10884  apexp1  10952  fihashf1rn  11022  lswlgt0cl  11137  ccatalpha  11161  pfxfv  11231  pfxsuff1eqwrdeq  11246  ccatopth2  11264  swrdccat  11282  swrdccat3blem  11286  reuccatpfxs1lem  11293  cjre  11408  caucvgre  11507  icodiamlt  11706  zsumdc  11910  zproddc  12105  reeff1  12226  dvdsmod0  12319  dvds2lem  12329  muldvds1  12342  dvdscmulr  12346  dvdsmulcr  12347  dvdsdivcl  12376  oddnn02np1  12406  ndvdsadd  12457  bitsinv1lem  12487  zeqzmulgcd  12506  bezoutlemmain  12534  dfgcd2  12550  gcdmultiple  12556  coprmdvds  12629  divgcdodd  12680  isprm6  12684  prmdvdsexpr  12687  cncongrprm  12694  phiprmpw  12759  modprm0  12792  pythagtriplem4  12806  pcz  12870  difsqpwdvds  12876  pcadd  12878  1arith  12905  isgrpid2  13588  ghmghmrn  13815  ghmf1  13825  kerf1ghm  13826  imasabl  13888  ringinvnz1ne0  14027  subrngringnsg  14184  domnmuln0  14252  rnglidlmcl  14459  znf1o  14630  znidom  14636  lmss  14935  cnplimcim  15356  dvcn  15389  fsumdvdsmul  15680  gausslemma2dlem1a  15752  lgseisenlem2  15765  lgsquad2  15777  2lgslem1b  15783  2sqlem6  15814  upgrpredgv  15959  upgredgpr  15962  wlkpropg  16065  upgrwlkcompim  16103  uspgr2wlkeq  16106  wlklenvclwlk  16114  wlkres  16118  clwwlk1loop  16136  umgrclwwlkge2  16139  ch2var  16186  bj-rspgt  16205  bj-charfundcALT  16227  bj-nntrans  16369  bj-nnelirr  16371  bj-omtrans  16374  setindft  16383  bj-inf2vnlem3  16390  bj-inf2vnlem4  16391  bj-findis  16397  pw1nct  16428