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  674  mtbiri  676  orbi2d  791  pm5.15dc  1400  exlimd2  1606  exintr  1645  19.9d  1672  19.23t  1688  chvarfv  1711  dral1  1741  spimt  1747  cbvalv1  1762  cbvalh  1764  chvar  1768  exdistrfor  1811  sbequi  1850  spv  1871  cbvexvw  1932  eqrdav  2192  cleqh  2293  ceqsalg  2788  vtoclf  2813  vtocl2  2815  vtocl3  2816  spcdv  2845  rspcdv  2867  elabgt  2901  sbcn1  3033  sbcim1  3034  sbcbi1  3035  sbeqalb  3042  sbcel21v  3050  eqrd  3197  exmidsssn  4231  exmidsssnc  4232  copsexg  4273  euotd  4283  rexxfrd  4494  relop  4812  elres  4978  rnxpid  5100  relcnvtr  5185  iotaval  5226  mpteqb  5648  elfvmptrab  5653  chfnrn  5669  elpreima  5677  ffnfv  5716  f1elima  5816  f1eqcocnv  5834  fliftfun  5839  isoresbr  5852  isotr  5859  ovmpodv2  6052  smoiso  6355  nnaordi  6561  nnaword  6564  nnawordi  6568  xpider  6660  iinerm  6661  mptelixpg  6788  dom2lem  6826  nneneq  6913  exmidpw  6964  infidc  6993  f1dmvrnfibi  7003  ismkvnex  7214  pr2nelem  7251  exmidfodomrlemeldju  7259  exmidfodomrlemreseldju  7260  netap  7314  2omotaplemap  7317  addcanpig  7394  mulcanpig  7395  enqer  7418  ltexnqi  7469  prarloclemlo  7554  genpcdl  7579  genpcuu  7580  appdivnq  7623  ltprordil  7649  1idprl  7650  1idpru  7651  ltexprlemm  7660  ltexprlemopu  7663  ltexprlemru  7672  cauappcvgprlemladdru  7716  cauappcvgprlemladdrl  7717  caucvgprprlemopu  7759  caucvgsrlemoffcau  7858  caucvgsrlemoffres  7860  ltrenn  7915  axpre-ltadd  7946  addn0nid  8393  apne  8642  aptap  8669  prodgt02  8872  prodge02  8874  mulgt1  8882  divgt0  8891  divge0  8892  cju  8980  nnsub  9021  nominpos  9220  zltnle  9363  nn0n0n1ge2  9387  zdcle  9393  btwnnz  9411  uzm1  9623  supinfneg  9660  infsupneg  9661  ublbneg  9678  cnref1o  9716  ltsubrp  9756  ltaddrp  9757  xnn0dcle  9868  npnflt  9881  nmnfgt  9884  ge0nemnf  9890  xltnegi  9901  xnn0xadd0  9933  iccsupr  10032  icoshft  10056  iccshftri  10061  iccshftli  10063  iccdili  10065  icccntri  10067  fzdcel  10106  fznlem  10107  fzen  10109  fzofzim  10255  eluzgtdifelfzo  10264  elfzonelfzo  10297  qltnle  10313  addmodlteq  10469  qsqeqor  10721  apexp1  10789  fihashf1rn  10859  cjre  11026  caucvgre  11125  icodiamlt  11324  zsumdc  11527  zproddc  11722  reeff1  11843  dvdsmod0  11936  dvds2lem  11946  muldvds1  11959  dvdscmulr  11963  dvdsmulcr  11964  dvdsdivcl  11992  oddnn02np1  12021  ndvdsadd  12072  zeqzmulgcd  12107  bezoutlemmain  12135  dfgcd2  12151  gcdmultiple  12157  coprmdvds  12230  divgcdodd  12281  isprm6  12285  prmdvdsexpr  12288  cncongrprm  12295  phiprmpw  12360  modprm0  12392  pythagtriplem4  12406  pcz  12470  difsqpwdvds  12476  pcadd  12478  1arith  12505  isgrpid2  13112  ghmghmrn  13333  ghmf1  13343  kerf1ghm  13344  imasabl  13406  ringinvnz1ne0  13545  subrngringnsg  13701  domnmuln0  13769  rnglidlmcl  13976  znf1o  14139  znidom  14145  lmss  14414  cnplimcim  14821  dvcn  14849  gausslemma2dlem1a  15174  lgseisenlem2  15187  2sqlem6  15207  ch2var  15259  bj-rspgt  15278  bj-charfundcALT  15301  bj-nntrans  15443  bj-nnelirr  15445  bj-omtrans  15448  setindft  15457  bj-inf2vnlem3  15464  bj-inf2vnlem4  15465  bj-findis  15471  pw1nct  15493