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  7496  pr2nelem  7538  exmidfodomrlemeldju  7552  exmidfodomrlemreseldju  7553  netap  7621  2omotaplemap  7624  addcanpig  7702  mulcanpig  7703  enqer  7726  ltexnqi  7777  prarloclemlo  7862  genpcdl  7887  genpcuu  7888  appdivnq  7931  ltprordil  7957  1idprl  7958  1idpru  7959  ltexprlemm  7968  ltexprlemopu  7971  ltexprlemru  7980  cauappcvgprlemladdru  8024  cauappcvgprlemladdrl  8025  caucvgprprlemopu  8067  caucvgsrlemoffcau  8166  caucvgsrlemoffres  8168  ltrenn  8223  axpre-ltadd  8254  addn0nid  8702  apne  8954  aptap  8981  prodgt02  9186  prodge02  9188  mulgt1  9196  divgt0  9205  divge0  9206  cju  9294  nnsub  9346  nominpos  9548  zltnle  9695  nn0n0n1ge2  9720  zdcle  9726  btwnnz  9745  uzm1  9963  supinfneg  10005  infsupneg  10006  ublbneg  10023  cnref1o  10062  ltsubrp  10102  ltaddrp  10103  xnn0dcle  10215  npnflt  10228  nmnfgt  10231  ge0nemnf  10237  xltnegi  10248  xnn0xadd0  10280  iccsupr  10379  icoshft  10403  iccshftri  10408  iccshftli  10410  iccdili  10412  icccntri  10414  fzdcel  10455  fznlem  10456  fzen  10458  fzofzim  10611  eluzgtdifelfzo  10626  elfzonelfzo  10659  qltnle  10689  addmodlteq  10850  qsqeqor  11102  apexp1  11172  fihashf1rn  11243  lswlgt0cl  11373  ccatalpha  11397  pfxfv  11472  pfxsuff1eqwrdeq  11487  ccatopth2  11505  swrdccat  11523  swrdccat3blem  11527  reuccatpfxs1lem  11534  cjre  11663  caucvgre  11763  icodiamlt  11963  zsumdc  12170  zproddc  12365  reeff1  12486  dvdsmod0  12579  dvds2lem  12589  muldvds1  12602  dvdscmulr  12606  dvdsmulcr  12607  dvdsdivcl  12636  oddnn02np1  12666  ndvdsadd  12717  bitsinv1lem  12747  zeqzmulgcd  12766  bezoutlemmain  12794  dfgcd2  12810  gcdmultiple  12816  coprmdvds  12889  divgcdodd  12941  isprm6  12945  prmdvdsexpr  12948  cncongrprm  12955  phiprmpw  13023  modprm0  13056  pythagtriplem4  13070  pcz  13134  difsqpwdvds  13140  pcadd  13142  1arith  13169  ballotfilemfc0  13284  ballotfilemfcc  13285  isgrpid2  13898  ghmghmrn  14119  ghmf1  14129  kerf1ghm  14130  imasabl  14224  rng1zrlem  14342  ringinvnz1ne0  14438  subrngringnsg  14597  domnmuln0  14666  rnglidlmcl  14901  znf1o  15070  znidom  15076  lmss  15438  cnplimcim  15859  dvcn  15892  fsumdvdsmul  16246  bposlem7  16278  gausslemma2dlem1a  16343  lgseisenlem2  16356  lgsquad2  16368  2lgslem1b  16374  2sqlem6  16405  upgrpredgv  16553  upgredgpr  16556  uhgr0v0e  16641  subgrprop  16666  wlkpropg  16731  upgrwlkcompim  16769  uspgr2wlkeq  16772  wlklenvclwlk  16780  wlkres  16786  clwwlk1loop  16806  umgrclwwlkge2  16809  clwwlkn1loopb  16827  clwwlknonex2lem2  16845  ch2var  16961  bj-rspgt  16980  bj-charfundcALT  17001  bj-nntrans  17143  bj-nnelirr  17145  bj-omtrans  17148  setindft  17157  bj-inf2vnlem3  17164  bj-inf2vnlem4  17165  bj-findis  17171  pw1nct  17199