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  1408  exlimd2  1617  exintr  1656  19.9d  1683  19.23t  1699  chvarfv  1722  dral1  1752  spimt  1758  cbvalv1  1773  cbvalh  1775  chvar  1779  exdistrfor  1822  sbequi  1861  spv  1882  cbvexvw  1943  eqrdav  2203  cleqh  2304  ceqsalg  2799  vtoclf  2825  vtocl2  2827  vtocl3  2828  spcdv  2857  rspcdv  2879  elabgt  2913  sbcn1  3045  sbcim1  3046  sbcbi1  3047  sbeqalb  3054  sbcel21v  3062  eqrd  3210  exmidsssn  4245  exmidsssnc  4246  copsexg  4287  euotd  4298  rexxfrd  4509  relop  4827  elres  4994  rnxpid  5116  relcnvtr  5201  iotaval  5242  mpteqb  5669  elfvmptrab  5674  chfnrn  5690  elpreima  5698  ffnfv  5737  f1elima  5841  f1eqcocnv  5859  fliftfun  5864  isoresbr  5877  isotr  5884  ovmpodv2  6078  smoiso  6387  nnaordi  6593  nnaword  6596  nnawordi  6600  xpider  6692  iinerm  6693  mptelixpg  6820  dom2lem  6862  nneneq  6953  exmidpw  7004  infidc  7035  f1dmvrnfibi  7045  ismkvnex  7256  pr2nelem  7298  exmidfodomrlemeldju  7306  exmidfodomrlemreseldju  7307  netap  7365  2omotaplemap  7368  addcanpig  7446  mulcanpig  7447  enqer  7470  ltexnqi  7521  prarloclemlo  7606  genpcdl  7631  genpcuu  7632  appdivnq  7675  ltprordil  7701  1idprl  7702  1idpru  7703  ltexprlemm  7712  ltexprlemopu  7715  ltexprlemru  7724  cauappcvgprlemladdru  7768  cauappcvgprlemladdrl  7769  caucvgprprlemopu  7811  caucvgsrlemoffcau  7910  caucvgsrlemoffres  7912  ltrenn  7967  axpre-ltadd  7998  addn0nid  8445  apne  8695  aptap  8722  prodgt02  8925  prodge02  8927  mulgt1  8935  divgt0  8944  divge0  8945  cju  9033  nnsub  9074  nominpos  9274  zltnle  9417  nn0n0n1ge2  9442  zdcle  9448  btwnnz  9466  uzm1  9678  supinfneg  9715  infsupneg  9716  ublbneg  9733  cnref1o  9771  ltsubrp  9811  ltaddrp  9812  xnn0dcle  9923  npnflt  9936  nmnfgt  9939  ge0nemnf  9945  xltnegi  9956  xnn0xadd0  9988  iccsupr  10087  icoshft  10111  iccshftri  10116  iccshftli  10118  iccdili  10120  icccntri  10122  fzdcel  10161  fznlem  10162  fzen  10164  fzofzim  10310  eluzgtdifelfzo  10324  elfzonelfzo  10357  qltnle  10384  addmodlteq  10541  qsqeqor  10793  apexp1  10861  fihashf1rn  10931  lswlgt0cl  11043  cjre  11135  caucvgre  11234  icodiamlt  11433  zsumdc  11637  zproddc  11832  reeff1  11953  dvdsmod0  12046  dvds2lem  12056  muldvds1  12069  dvdscmulr  12073  dvdsmulcr  12074  dvdsdivcl  12103  oddnn02np1  12133  ndvdsadd  12184  bitsinv1lem  12214  zeqzmulgcd  12233  bezoutlemmain  12261  dfgcd2  12277  gcdmultiple  12283  coprmdvds  12356  divgcdodd  12407  isprm6  12411  prmdvdsexpr  12414  cncongrprm  12421  phiprmpw  12486  modprm0  12519  pythagtriplem4  12533  pcz  12597  difsqpwdvds  12603  pcadd  12605  1arith  12632  isgrpid2  13314  ghmghmrn  13541  ghmf1  13551  kerf1ghm  13552  imasabl  13614  ringinvnz1ne0  13753  subrngringnsg  13909  domnmuln0  13977  rnglidlmcl  14184  znf1o  14355  znidom  14361  lmss  14660  cnplimcim  15081  dvcn  15114  fsumdvdsmul  15405  gausslemma2dlem1a  15477  lgseisenlem2  15490  lgsquad2  15502  2lgslem1b  15508  2sqlem6  15539  ch2var  15636  bj-rspgt  15655  bj-charfundcALT  15678  bj-nntrans  15820  bj-nnelirr  15822  bj-omtrans  15825  setindft  15834  bj-inf2vnlem3  15841  bj-inf2vnlem4  15842  bj-findis  15848  pw1nct  15873