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  4287  exmidsssnc  4288  copsexg  4331  euotd  4342  rexxfrd  4555  relop  4875  reldmm  4945  elres  5044  rnxpid  5166  relcnvtr  5251  iotaval  5293  mpteqb  5730  elfvmptrab  5735  chfnrn  5751  elpreima  5759  ffnfv  5798  f1elima  5906  f1eqcocnv  5924  fliftfun  5929  isoresbr  5942  isotr  5949  ovmpodv2  6147  smoiso  6459  nnaordi  6667  nnaword  6670  nnawordi  6674  xpider  6766  iinerm  6767  mptelixpg  6894  dom2lem  6936  nneneq  7031  exmidpw  7086  infidc  7117  f1dmvrnfibi  7127  ismkvnex  7338  pr2nelem  7380  exmidfodomrlemeldju  7393  exmidfodomrlemreseldju  7394  netap  7456  2omotaplemap  7459  addcanpig  7537  mulcanpig  7538  enqer  7561  ltexnqi  7612  prarloclemlo  7697  genpcdl  7722  genpcuu  7723  appdivnq  7766  ltprordil  7792  1idprl  7793  1idpru  7794  ltexprlemm  7803  ltexprlemopu  7806  ltexprlemru  7815  cauappcvgprlemladdru  7859  cauappcvgprlemladdrl  7860  caucvgprprlemopu  7902  caucvgsrlemoffcau  8001  caucvgsrlemoffres  8003  ltrenn  8058  axpre-ltadd  8089  addn0nid  8536  apne  8786  aptap  8813  prodgt02  9016  prodge02  9018  mulgt1  9026  divgt0  9035  divge0  9036  cju  9124  nnsub  9165  nominpos  9365  zltnle  9508  nn0n0n1ge2  9533  zdcle  9539  btwnnz  9557  uzm1  9770  supinfneg  9807  infsupneg  9808  ublbneg  9825  cnref1o  9863  ltsubrp  9903  ltaddrp  9904  xnn0dcle  10015  npnflt  10028  nmnfgt  10031  ge0nemnf  10037  xltnegi  10048  xnn0xadd0  10080  iccsupr  10179  icoshft  10203  iccshftri  10208  iccshftli  10210  iccdili  10212  icccntri  10214  fzdcel  10253  fznlem  10254  fzen  10256  fzofzim  10405  eluzgtdifelfzo  10420  elfzonelfzo  10453  qltnle  10480  addmodlteq  10637  qsqeqor  10889  apexp1  10957  fihashf1rn  11027  lswlgt0cl  11142  ccatalpha  11166  pfxfv  11237  pfxsuff1eqwrdeq  11252  ccatopth2  11270  swrdccat  11288  swrdccat3blem  11292  reuccatpfxs1lem  11299  cjre  11414  caucvgre  11513  icodiamlt  11712  zsumdc  11916  zproddc  12111  reeff1  12232  dvdsmod0  12325  dvds2lem  12335  muldvds1  12348  dvdscmulr  12352  dvdsmulcr  12353  dvdsdivcl  12382  oddnn02np1  12412  ndvdsadd  12463  bitsinv1lem  12493  zeqzmulgcd  12512  bezoutlemmain  12540  dfgcd2  12556  gcdmultiple  12562  coprmdvds  12635  divgcdodd  12686  isprm6  12690  prmdvdsexpr  12693  cncongrprm  12700  phiprmpw  12765  modprm0  12798  pythagtriplem4  12812  pcz  12876  difsqpwdvds  12882  pcadd  12884  1arith  12911  isgrpid2  13594  ghmghmrn  13821  ghmf1  13831  kerf1ghm  13832  imasabl  13894  ringinvnz1ne0  14033  subrngringnsg  14190  domnmuln0  14258  rnglidlmcl  14465  znf1o  14636  znidom  14642  lmss  14941  cnplimcim  15362  dvcn  15395  fsumdvdsmul  15686  gausslemma2dlem1a  15758  lgseisenlem2  15771  lgsquad2  15783  2lgslem1b  15789  2sqlem6  15820  upgrpredgv  15965  upgredgpr  15968  uhgr0v0e  16053  wlkpropg  16096  upgrwlkcompim  16134  uspgr2wlkeq  16137  wlklenvclwlk  16145  wlkres  16149  clwwlk1loop  16168  umgrclwwlkge2  16171  clwwlkn1loopb  16188  ch2var  16240  bj-rspgt  16259  bj-charfundcALT  16281  bj-nntrans  16423  bj-nnelirr  16425  bj-omtrans  16428  setindft  16437  bj-inf2vnlem3  16444  bj-inf2vnlem4  16445  bj-findis  16451  pw1nct  16482