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  1778  spimt  1784  cbvalv1  1799  cbvalh  1801  chvar  1805  exdistrfor  1848  sbequi  1887  spv  1908  cbvexvw  1969  eqrdav  2230  cleqh  2331  ceqsalg  2832  vtoclf  2858  vtocl2  2860  vtocl3  2861  spcdv  2892  rspcdv  2914  elabgt  2948  sbcn1  3080  sbcim1  3081  sbcbi1  3082  sbeqalb  3089  sbcel21v  3097  eqrd  3246  rabsnifsb  3741  exmidsssn  4298  exmidsssnc  4299  copsexg  4342  euotd  4353  rexxfrd  4566  relop  4886  reldmm  4956  elres  5055  rnxpid  5178  relcnvtr  5263  iotaval  5305  mpteqb  5746  elfvmptrab  5751  chfnrn  5767  elpreima  5775  ffnfv  5813  f1elima  5924  f1eqcocnv  5942  fliftfun  5947  isoresbr  5960  isotr  5967  ovmpodv2  6165  ressuppss  6432  funsssuppss  6436  smoiso  6511  nnaordi  6719  nnaword  6722  nnawordi  6726  xpider  6818  iinerm  6819  mptelixpg  6946  dom2lem  6988  nneneq  7086  exmidpw  7143  infidc  7176  f1dmvrnfibi  7186  ismkvnex  7397  pr2nelem  7439  exmidfodomrlemeldju  7453  exmidfodomrlemreseldju  7454  netap  7516  2omotaplemap  7519  addcanpig  7597  mulcanpig  7598  enqer  7621  ltexnqi  7672  prarloclemlo  7757  genpcdl  7782  genpcuu  7783  appdivnq  7826  ltprordil  7852  1idprl  7853  1idpru  7854  ltexprlemm  7863  ltexprlemopu  7866  ltexprlemru  7875  cauappcvgprlemladdru  7919  cauappcvgprlemladdrl  7920  caucvgprprlemopu  7962  caucvgsrlemoffcau  8061  caucvgsrlemoffres  8063  ltrenn  8118  axpre-ltadd  8149  addn0nid  8595  apne  8845  aptap  8872  prodgt02  9075  prodge02  9077  mulgt1  9085  divgt0  9094  divge0  9095  cju  9183  nnsub  9224  nominpos  9424  zltnle  9569  nn0n0n1ge2  9594  zdcle  9600  btwnnz  9618  uzm1  9831  supinfneg  9873  infsupneg  9874  ublbneg  9891  cnref1o  9929  ltsubrp  9969  ltaddrp  9970  xnn0dcle  10081  npnflt  10094  nmnfgt  10097  ge0nemnf  10103  xltnegi  10114  xnn0xadd0  10146  iccsupr  10245  icoshft  10269  iccshftri  10274  iccshftli  10276  iccdili  10278  icccntri  10280  fzdcel  10320  fznlem  10321  fzen  10323  fzofzim  10473  eluzgtdifelfzo  10488  elfzonelfzo  10521  qltnle  10549  addmodlteq  10706  qsqeqor  10958  apexp1  11026  fihashf1rn  11096  lswlgt0cl  11215  ccatalpha  11239  pfxfv  11314  pfxsuff1eqwrdeq  11329  ccatopth2  11347  swrdccat  11365  swrdccat3blem  11369  reuccatpfxs1lem  11376  cjre  11505  caucvgre  11604  icodiamlt  11803  zsumdc  12008  zproddc  12203  reeff1  12324  dvdsmod0  12417  dvds2lem  12427  muldvds1  12440  dvdscmulr  12444  dvdsmulcr  12445  dvdsdivcl  12474  oddnn02np1  12504  ndvdsadd  12555  bitsinv1lem  12585  zeqzmulgcd  12604  bezoutlemmain  12632  dfgcd2  12648  gcdmultiple  12654  coprmdvds  12727  divgcdodd  12778  isprm6  12782  prmdvdsexpr  12785  cncongrprm  12792  phiprmpw  12857  modprm0  12890  pythagtriplem4  12904  pcz  12968  difsqpwdvds  12974  pcadd  12976  1arith  13003  isgrpid2  13686  ghmghmrn  13913  ghmf1  13923  kerf1ghm  13924  imasabl  13986  ringinvnz1ne0  14126  subrngringnsg  14283  domnmuln0  14352  rnglidlmcl  14559  znf1o  14730  znidom  14736  lmss  15040  cnplimcim  15461  dvcn  15494  fsumdvdsmul  15788  gausslemma2dlem1a  15860  lgseisenlem2  15873  lgsquad2  15885  2lgslem1b  15891  2sqlem6  15922  upgrpredgv  16070  upgredgpr  16073  uhgr0v0e  16158  subgrprop  16183  wlkpropg  16248  upgrwlkcompim  16286  uspgr2wlkeq  16289  wlklenvclwlk  16297  wlkres  16303  clwwlk1loop  16323  umgrclwwlkge2  16326  clwwlkn1loopb  16344  clwwlknonex2lem2  16362  ch2var  16468  bj-rspgt  16487  bj-charfundcALT  16508  bj-nntrans  16650  bj-nnelirr  16652  bj-omtrans  16655  setindft  16664  bj-inf2vnlem3  16671  bj-inf2vnlem4  16672  bj-findis  16678  pw1nct  16708