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 ⊢ (𝜑 → (𝜓 → 𝜒))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used by:  mpbid  147  sylibd  149  sylbid  150  mpbidi  151  imbitrid  154  biimtrdi  163  ibi  176  imbi1d  231  biimpa  296  mtbird  684  mtbiri  686  orbi2d  802  pm5.15dc  1438  exlimd2  1648  exintr  1687  19.9d  1713  19.23t  1729  chvarfv  1752  dral1  1783  spimt  1789  cbvalv1  1804  cbvalh  1806  chvar  1810  exdistrfor  1853  sbequi  1892  spv  1913  cbvexvw  1976  eqrdav  2237  cleqh  2338  ceqsalg  2850  vtoclf  2876  vtocl2  2878  vtocl3  2879  spcdv  2910  rspcdv  2932  elabgt  2967  sbcn1  3099  sbcim1  3100  sbcbi1  3101  sbeqalb  3108  sbcel21v  3116  eqrd  3266  ifeqeqxdc  3687  rabsnifsb  3777  exmidsssn  4339  exmidsssnc  4340  copsexg  4384  euotd  4395  rexxfrd  4609  relop  4930  reldmm  5000  elres  5099  rnxpid  5222  relcnvtr  5307  iotaval  5349  mpteqb  5796  elfvmptrab  5802  chfnrn  5820  elpreima  5828  ffnfv  5866  f1elima  5979  f1eqcocnv  5997  fliftfun  6002  isoresbr  6015  isotr  6022  ovmpodv2  6222  ressuppss  6494  funsssuppss  6498  smoiso  6573  nnaordi  6781  nnaword  6784  nnawordi  6788  xpider  6880  iinerm  6881  mptelixpg  7016  dom2lem  7058  nneneq  7158  exmidpw  7215  infidc  7248  f1dmvrnfibi  7258  fsuppimp  7292  ismkvnex  7495  pr2nelem  7537  exmidfodomrlemeldju  7551  exmidfodomrlemreseldju  7552  netap  7620  2omotaplemap  7623  addcanpig  7701  mulcanpig  7702  enqer  7725  ltexnqi  7776  prarloclemlo  7861  genpcdl  7886  genpcuu  7887  appdivnq  7930  ltprordil  7956  1idprl  7957  1idpru  7958  ltexprlemm  7967  ltexprlemopu  7970  ltexprlemru  7979  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  caucvgprprlemopu  8066  caucvgsrlemoffcau  8165  caucvgsrlemoffres  8167  ltrenn  8222  axpre-ltadd  8253  addn0nid  8701  apne  8953  aptap  8980  prodgt02  9185  prodge02  9187  mulgt1  9195  divgt0  9204  divge0  9205  cju  9293  nnsub  9345  nominpos  9547  zltnle  9694  nn0n0n1ge2  9719  zdcle  9725  btwnnz  9744  uzm1  9962  supinfneg  10004  infsupneg  10005  ublbneg  10022  cnref1o  10061  ltsubrp  10101  ltaddrp  10102  xnn0dcle  10214  npnflt  10227  nmnfgt  10230  ge0nemnf  10236  xltnegi  10247  xnn0xadd0  10279  iccsupr  10378  icoshft  10402  iccshftri  10407  iccshftli  10409  iccdili  10411  icccntri  10413  fzdcel  10454  fznlem  10455  fzen  10457  fzofzim  10610  eluzgtdifelfzo  10625  elfzonelfzo  10658  qltnle  10688  addmodlteq  10848  qsqeqor  11100  apexp1  11170  fihashf1rn  11241  lswlgt0cl  11371  ccatalpha  11395  pfxfv  11470  pfxsuff1eqwrdeq  11485  ccatopth2  11503  swrdccat  11521  swrdccat3blem  11525  reuccatpfxs1lem  11532  cjre  11661  caucvgre  11761  icodiamlt  11961  zsumdc  12167  zproddc  12362  reeff1  12483  dvdsmod0  12576  dvds2lem  12586  muldvds1  12599  dvdscmulr  12603  dvdsmulcr  12604  dvdsdivcl  12633  oddnn02np1  12663  ndvdsadd  12714  bitsinv1lem  12744  zeqzmulgcd  12763  bezoutlemmain  12791  dfgcd2  12807  gcdmultiple  12813  coprmdvds  12886  divgcdodd  12938  isprm6  12942  prmdvdsexpr  12945  cncongrprm  12952  phiprmpw  13020  modprm0  13053  pythagtriplem4  13067  pcz  13131  difsqpwdvds  13137  pcadd  13139  1arith  13166  ballotfilemfc0  13281  ballotfilemfcc  13282  isgrpid2  13894  ghmghmrn  14115  ghmf1  14125  kerf1ghm  14126  imasabl  14189  rng1zrlem  14307  ringinvnz1ne0  14403  subrngringnsg  14562  domnmuln0  14631  rnglidlmcl  14866  znf1o  15035  znidom  15041  lmss  15396  cnplimcim  15817  dvcn  15850  fsumdvdsmul  16186  gausslemma2dlem1a  16275  lgseisenlem2  16288  lgsquad2  16300  2lgslem1b  16306  2sqlem6  16337  upgrpredgv  16485  upgredgpr  16488  uhgr0v0e  16573  subgrprop  16598  wlkpropg  16663  upgrwlkcompim  16701  uspgr2wlkeq  16704  wlklenvclwlk  16712  wlkres  16718  clwwlk1loop  16738  umgrclwwlkge2  16741  clwwlkn1loopb  16759  clwwlknonex2lem2  16777  ch2var  16893  bj-rspgt  16912  bj-charfundcALT  16933  bj-nntrans  17075  bj-nnelirr  17077  bj-omtrans  17080  setindft  17089  bj-inf2vnlem3  17096  bj-inf2vnlem4  17097  bj-findis  17103  pw1nct  17131