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  679  mtbiri  681  orbi2d  797  pm5.15dc  1433  exlimd2  1643  exintr  1682  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  2831  vtoclf  2857  vtocl2  2859  vtocl3  2860  spcdv  2891  rspcdv  2913  elabgt  2947  sbcn1  3079  sbcim1  3080  sbcbi1  3081  sbeqalb  3088  sbcel21v  3096  eqrd  3245  rabsnifsb  3737  exmidsssn  4292  exmidsssnc  4293  copsexg  4336  euotd  4347  rexxfrd  4560  relop  4880  reldmm  4950  elres  5049  rnxpid  5171  relcnvtr  5256  iotaval  5298  mpteqb  5737  elfvmptrab  5742  chfnrn  5758  elpreima  5766  ffnfv  5805  f1elima  5914  f1eqcocnv  5932  fliftfun  5937  isoresbr  5950  isotr  5957  ovmpodv2  6155  smoiso  6468  nnaordi  6676  nnaword  6679  nnawordi  6683  xpider  6775  iinerm  6776  mptelixpg  6903  dom2lem  6945  nneneq  7043  exmidpw  7100  infidc  7133  f1dmvrnfibi  7143  ismkvnex  7354  pr2nelem  7396  exmidfodomrlemeldju  7410  exmidfodomrlemreseldju  7411  netap  7473  2omotaplemap  7476  addcanpig  7554  mulcanpig  7555  enqer  7578  ltexnqi  7629  prarloclemlo  7714  genpcdl  7739  genpcuu  7740  appdivnq  7783  ltprordil  7809  1idprl  7810  1idpru  7811  ltexprlemm  7820  ltexprlemopu  7823  ltexprlemru  7832  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  caucvgprprlemopu  7919  caucvgsrlemoffcau  8018  caucvgsrlemoffres  8020  ltrenn  8075  axpre-ltadd  8106  addn0nid  8553  apne  8803  aptap  8830  prodgt02  9033  prodge02  9035  mulgt1  9043  divgt0  9052  divge0  9053  cju  9141  nnsub  9182  nominpos  9382  zltnle  9525  nn0n0n1ge2  9550  zdcle  9556  btwnnz  9574  uzm1  9787  supinfneg  9829  infsupneg  9830  ublbneg  9847  cnref1o  9885  ltsubrp  9925  ltaddrp  9926  xnn0dcle  10037  npnflt  10050  nmnfgt  10053  ge0nemnf  10059  xltnegi  10070  xnn0xadd0  10102  iccsupr  10201  icoshft  10225  iccshftri  10230  iccshftli  10232  iccdili  10234  icccntri  10236  fzdcel  10275  fznlem  10276  fzen  10278  fzofzim  10428  eluzgtdifelfzo  10443  elfzonelfzo  10476  qltnle  10504  addmodlteq  10661  qsqeqor  10913  apexp1  10981  fihashf1rn  11051  lswlgt0cl  11170  ccatalpha  11194  pfxfv  11269  pfxsuff1eqwrdeq  11284  ccatopth2  11302  swrdccat  11320  swrdccat3blem  11324  reuccatpfxs1lem  11331  cjre  11447  caucvgre  11546  icodiamlt  11745  zsumdc  11950  zproddc  12145  reeff1  12266  dvdsmod0  12359  dvds2lem  12369  muldvds1  12382  dvdscmulr  12386  dvdsmulcr  12387  dvdsdivcl  12416  oddnn02np1  12446  ndvdsadd  12497  bitsinv1lem  12527  zeqzmulgcd  12546  bezoutlemmain  12574  dfgcd2  12590  gcdmultiple  12596  coprmdvds  12669  divgcdodd  12720  isprm6  12724  prmdvdsexpr  12727  cncongrprm  12734  phiprmpw  12799  modprm0  12832  pythagtriplem4  12846  pcz  12910  difsqpwdvds  12916  pcadd  12918  1arith  12945  isgrpid2  13628  ghmghmrn  13855  ghmf1  13865  kerf1ghm  13866  imasabl  13928  ringinvnz1ne0  14068  subrngringnsg  14225  domnmuln0  14293  rnglidlmcl  14500  znf1o  14671  znidom  14677  lmss  14976  cnplimcim  15397  dvcn  15430  fsumdvdsmul  15721  gausslemma2dlem1a  15793  lgseisenlem2  15806  lgsquad2  15818  2lgslem1b  15824  2sqlem6  15855  upgrpredgv  16003  upgredgpr  16006  uhgr0v0e  16091  subgrprop  16116  wlkpropg  16181  upgrwlkcompim  16219  uspgr2wlkeq  16222  wlklenvclwlk  16230  wlkres  16236  clwwlk1loop  16256  umgrclwwlkge2  16259  clwwlkn1loopb  16277  clwwlknonex2lem2  16295  ch2var  16389  bj-rspgt  16408  bj-charfundcALT  16430  bj-nntrans  16572  bj-nnelirr  16574  bj-omtrans  16577  setindft  16586  bj-inf2vnlem3  16593  bj-inf2vnlem4  16594  bj-findis  16600  pw1nct  16630