Theorem biimpd 229

Description: Deduce an implication from a logical equivalence. Deduction associated with biimp 215 and biimpi 216. (Contributed by NM, 11-Jan-1993.)

Hypothesis

Ref	Expression
biimpd.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
biimpd	⊢ (𝜑 → (𝜓 → 𝜒))

Proof of Theorem biimpd

Step	Hyp	Ref	Expression
1		biimpd.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		biimp 215	. 2 ⊢ ((𝜓 ↔ 𝜒) → (𝜓 → 𝜒))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝜓 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  mpbid  232  sylibd  239  sylbid  240  mpbidi  241  imbitrid  244  biimtrdi  253  con4bid  317  mtbird  325  mtbiri  327  imbi1d  341  bitr3  352  pm5.21im  374  biimpa  476  alexbii  1831  spvv  1996  spfw  2032  cbvalw  2034  sbequi  2084  chvarfv  2241  cbvalv1  2347  spv  2401  chvar  2403  cbval  2406  sb1  2486  nfsb4t  2507  exmoeu  2584  euim  2620  2eu3  2657  eqrdav  2739  ralbida  3276  rgen2a  3379  ralcom2  3385  ceqsalt  3523  ceqsalgALT  3526  spcimgft  3558  vtoclfOLD  3577  vtoclegft  3601  spcdv  3607  rspcdv  3627  rspcebdv  3629  rexraleqim  3660  elabgtOLDOLD  3687  sbcn1  3860  sbcim1OLD  3862  sbcbi1  3866  sbeqalb  3872  sbcel21v  3877  disj  4473  elpwunsn  4707  rabsnifsb  4747  ssunsn2  4852  preqr1g  4877  iuneqconst  5026  axprlem3  5443  sbcop1  5508  propeqop  5526  euotd  5532  rexopabb  5547  sotr2  5641  relop  5875  elinxp  6048  elimasni  6121  sotri2  6161  onmindif  6487  iotavalOLD  6547  dffv2  7017  mpteqb  7048  elfvmptrab  7058  chfnrn  7082  elpreima  7091  iinpreima  7102  exfo  7139  ffnfv  7153  f1elima  7300  f1eqcocnv  7337  fliftfun  7348  soisores  7363  isotr  7372  isomin  7373  ovmpodv2  7608  difsnexi  7796  onint  7826  oneqmin  7836  ordunisuc2  7881  tfindsg  7898  findsg  7937  f1oweALT  8013  el2mpocl  8127  poseq  8199  soseq  8200  ressuppss  8224  funsssuppss  8231  suppofssd  8244  smoiso  8418  seqomlem2  8507  oaordi  8602  oawordri  8606  oaordex  8614  oalimcl  8616  omwordi  8627  oewordi  8647  oelim2  8651  nnmwordi  8691  xpider  8846  iiner  8847  undifixp  8992  mptelixpg  8993  dom2lem  9052  findcard2s  9231  pssnn  9234  nneneq  9272  nneneqOLD  9284  fineqvlem  9325  dif1ennnALT  9339  unfilem2  9372  xpfiOLD  9387  domunfican  9389  f1dmvrnfibi  9409  fsuppimp  9438  dffi2  9492  infsupprpr  9573  wemaplem2  9616  suc11reg  9688  noinfep  9729  cantnflem1  9758  r1fin  9842  tcrank  9953  cardlim  10041  pr2nelemOLD  10072  fseqenlem1  10093  alephnbtwn  10140  alephord2i  10146  alephf1  10154  cardaleph  10158  alephiso  10167  dfac12lem2  10214  ackbij1lem16  10303  cflm  10319  cfcoflem  10341  sornom  10346  fin23lem27  10397  isf32lem7  10428  fin17  10463  fin1a2lem2  10470  fin1a2lem4  10472  fin1a2lem6  10474  fin1a2lem9  10477  axdc3lem2  10520  zorn2lem7  10571  uniimadom  10613  inar1  10844  grothomex  10898  addcanpi  10968  mulcanpi  10969  enqer  10990  genpcd  11075  genpnmax  11076  ltexprlem4  11108  reclem3pr  11118  reclem4pr  11119  suplem2pr  11122  axpre-ltadd  11236  axpre-sup  11238  ltletr  11382  00id  11465  addn0nid  11710  mul0or  11930  prodgt02  12142  lemul1a  12148  mulgt1OLD  12153  divgt0  12163  divge0  12164  ledivp1i  12220  ltdivp1i  12221  cju  12289  nnsub  12337  nominpos  12530  nn0n0n1ge2  12620  btwnnz  12719  suprfinzcl  12757  ublbneg  12998  zmax  13010  cnref1o  13050  ltsubrp  13093  ltaddrp  13094  xrltletr  13219  qbtwnre  13261  xltnegi  13278  xnn0xadd0  13309  iccsupr  13502  icoshft  13533  difreicc  13544  iccshftri  13547  iccshftli  13549  iccdili  13551  icccntri  13553  fzen  13601  elfz1b  13653  fzofzim  13763  eluzgtdifelfzo  13778  elfzo1elm1fzo0  13818  injresinjlem  13837  injresinj  13838  flval2  13865  flval3  13866  modmuladdim  13965  modaddmodup  13985  addmodlteq  13997  fseqsupubi  14029  ssnn0fi  14036  mptnn0fsuppr  14050  sq01  14274  hashf1rn  14401  hashgt12el  14471  hashgt12el2  14472  hashfundm  14491  hash2pr  14518  hash2exprb  14520  hashge2el2difr  14530  hashtpg  14534  hash3tr  14540  lswlgt0cl  14617  ccatalpha  14641  pfxfv  14730  pfxsuff1eqwrdeq  14747  ccatopth2  14765  swrdccat  14783  swrdccat3blem  14787  reuccatpfxs1lem  14794  repsdf2  14826  repswsymball  14827  repswrevw  14835  cshweqrep  14869  cshw1  14870  2cshwcshw  14874  scshwfzeqfzo  14875  cshwcsh2id  14877  swrdco  14886  swrd2lsw  15001  2swrd2eqwrdeq  15002  wwlktovfo  15007  cjre  15188  icodiamlt  15484  reusq0  15511  o1lo1  15583  o1of2  15659  o1rlimmul  15665  zsum  15766  modfsummods  15841  zprod  15985  reeff1  16168  dvdsmod0  16308  dvds2lem  16317  muldvds1  16329  dvdscmulr  16333  dvdsmulcr  16334  dvdsdivcl  16364  mod2eq1n2dvds  16395  oddnn02np1  16396  divalglem8  16448  ndvdsadd  16458  zeqzmulgcd  16556  dfgcd2  16593  absproddvds  16664  lcmftp  16683  coprmdvds  16700  2mulprm  16740  isprm5  16754  divgcdodd  16757  isprm6  16761  prmdvdsexpr  16764  prmdvdsbc  16773  cncongrprm  16776  phiprmpw  16823  modprm0  16852  pythagtriplem4  16866  pcz  16928  difsqpwdvds  16934  1arith  16974  prmgaplem5  17102  prmgaplem6  17103  cshwrepswhash1  17150  sbcie2s  17208  divsfval  17607  catsubcat  17903  fthmon  17994  isinitoi  18066  istermoi  18067  iszeroi  18076  setcmon  18154  setcepi  18155  funcestrcsetclem8  18216  fthestrcsetc  18219  funcsetcestrclem8  18231  fthsetcestrc  18234  odupos  18398  pltnle  18408  pltval3  18409  lublecllem  18430  latasym  18513  mrelatglb  18630  mrelatlub  18632  cnvpsb  18649  mgmpropd  18689  isgrpid2  19016  ghmghmrn  19275  ghmf1  19286  kerf1ghm  19287  orbsta  19353  resscntz  19373  gsmsymgrfixlem1  19469  gsmsymgreqlem2  19473  mndodcongi  19585  odf1  19604  lsmss1  19707  lsmss2  19709  efgredeu  19794  cntzcmnss  19883  imasabl  19918  lt6abl  19937  ablfaclem3  20131  ringinvnz1ne0  20323  0ringnnzr  20551  subrngringnsg  20579  srhmsubc  20702  domnmuln0  20731  lspsneq  21147  lspsneu  21148  lsmcv  21166  rnglidlmcl  21249  rngqiprngimf1lem  21327  lidldvgen  21367  domnchr  21570  znf1o  21593  zntoslem  21598  znfld  21602  cygznlem2a  21609  cygznlem3  21611  phlssphl  21700  islindf4  21881  uvcendim  21890  psdmul  22193  ply1scln0  22316  gsummoncoe1  22333  matvscl  22458  scmataddcl  22543  scmatsubcl  22544  scmatfo  22557  scmatghm  22560  maducoeval2  22667  slesolinv  22707  cramerimplem2  22711  cpmatelimp  22739  cpmatelimp2  22741  cpmatacl  22743  cpmatinvcl  22744  pm2mpf1  22826  cayhamlem1  22893  cayleyhamilton1  22919  0ntr  23100  islpi  23178  lmss  23327  cmpcld  23431  cmpfi  23437  1stcelcls  23490  comppfsc  23561  ptcnplem  23650  qtophmeo  23846  fbdmn0  23863  fbasrn  23913  elfm3  23979  fmfnfmlem4  23986  fclscf  24054  cnpfcf  24070  alexsubALTlem3  24078  tsmsres  24173  blval2  24596  tnggrpr  24697  nmoleub  24773  nmhmcn  25172  ncvs1  25210  iscau4  25332  caussi  25350  cmssmscld  25403  cmslssbn  25425  cniccbdd  25515  ovoliunnul  25561  mbfinf  25719  itg2splitlem  25803  dvcn  25977  c1lip1  26056  c1lip3  26058  dvcnvrelem1  26076  dvfsumlem2  26087  ply1divex  26196  quotcan  26369  aannenlem1  26388  taylf  26420  taylthlem2  26434  ulmcaulem  26455  ulmcau  26456  reeff1o  26509  logccv  26723  rtprmirr  26821  logreclem  26823  isosctrlem2  26880  xrlimcnp  27029  rlimcxp  27035  ftalem7  27140  vmappw  27177  fsumdvdsmul  27256  fsumvma  27275  dchreq  27320  dchrptlem1  27326  dchrsum  27331  bposlem7  27352  lgsqrlem2  27409  lgsdchr  27417  gausslemma2dlem1a  27427  lgseisenlem2  27438  lgsquad2  27448  2lgslem1b  27454  2sqlem6  27485  2sqnn0  27500  addsq2reu  27502  2sqreulem2  27514  sltval2  27719  sltres  27725  nodenselem8  27754  nodense  27755  noresle  27760  scutun12  27873  madeval2  27910  elmade  27924  negsf1o  28104  muls0ord  28229  recsex  28261  noseqrdgfn  28330  n0subs  28378  eln0zs  28404  tgcgrcomimp  28503  isperp2  28741  xmstrkgc  28918  brbtwn  28932  brcgr  28933  axcgrid  28949  axeuclidlem  28995  axeuclid  28996  elntg2  29018  lpvtx  29103  upgrex  29127  upgrpredgv  29174  upgredgpr  29177  uhgr0v0e  29273  subgrprop  29308  fusgrfisbase  29363  edgnbusgreu  29402  nbusgredgeu0  29403  cusgredg  29459  structtocusgr  29481  cusgrsize2inds  29489  cusgrsize  29490  usgredgsscusgredg  29495  fusgrmaxsize  29500  uspgrloopvtxel  29552  umgr2v2e  29561  vtxdginducedm1fi  29580  finsumvtxdg2sstep  29585  rgrprop  29596  rusgrprop  29598  0uhgrrusgr  29614  rusgrpropedg  29620  ewlkprop  29639  upgrewlkle2  29642  wlkprop  29647  upgrwlkcompim  29679  uspgr2wlkeq  29682  wlklenvclwlk  29691  wlkonprop  29694  wlkres  29706  redwlk  29708  wlkdlem2  29719  wksonproplem  29740  wksonproplemOLD  29741  usgr2trlspth  29797  usgr2pth  29800  pthdlem1  29802  crctcshwlkn0lem4  29846  wwlksnprcl  29872  wlkiswwlks2  29908  wwlksm1edg  29914  wlknewwlksn  29920  wwlksnred  29925  wwlksnextbi  29927  wwlksnextwrd  29930  wwlksnextinj  29932  wwlksnextsurj  29933  umgr2wlk  29982  umgrwwlks2on  29990  elwwlks2  29999  clwwlk1loop  30020  umgrclwwlkge2  30023  clwlkclwwlklem2a1  30024  clwlkclwwlklem2a4  30029  clwlkclwwlklem2a  30030  clwlkclwwlklem2  30032  clwlkclwwlkfo  30041  clwwisshclwwslemlem  30045  clwwlknwwlksn  30070  clwwlknlbonbgr1  30071  clwwlkn1loopb  30075  clwwlkf  30079  clwwlknon1  30129  clwwlknonwwlknonb  30138  clwwlknonex2lem2  30140  vdn0conngrumgrv2  30228  frgrnbnb  30325  frgrncvvdeqlem2  30332  frgrncvvdeqlem3  30333  frgrncvvdeqlem6  30336  frgrwopreglem4a  30342  fusgr2wsp2nb  30366  frrusgrord0lem  30371  numclwwlk2lem1lem  30374  2clwwlk2clwwlklem  30378  2clwwlk2clwwlk  30382  numclwwlk1lem2foa  30386  numclwwlk1lem2f1  30389  frgrreg  30426  hlipgt0  30946  ocin  31328  ocnel  31330  shmodsi  31421  pjmf1  31748  unopf1o  31948  staddi  32278  stadd3i  32280  mdi  32327  dmdmd  32332  dmdi  32334  dmdbr2  32335  dmdbr3  32337  dmdbr4  32338  dmdi4  32339  mdsl1i  32353  superpos  32386  cvbr4i  32399  atssma  32410  atcv1  32412  atomli  32414  chirredlem1  32422  addltmulALT  32478  bian1dOLD  32485  ifeqeqx  32565  disjxpin  32610  suppss3  32738  fpwrelmap  32747  expgt0b  32820  mndlactfo  33013  mndractfo  33015  ogrpaddlt  33067  qsfld  33491  ply1degltdimlem  33635  ply1degltdim  33636  metider  33840  tpr2rico  33858  xrge0iifiso  33881  qqhcn  33937  qqhucn  33938  esumlub  34024  esumpinfval  34037  esumpinfsum  34041  ballotlemfc0  34457  ballotlemfcc  34458  ftc2re  34575  bnj517  34861  axsepg2  35058  axsepg2ALT  35059  fnrelpredd  35065  axnulg  35068  pfxwlk  35091  subgrwlk  35100  loop1cycl  35105  erdsze2lem2  35172  satfv1  35331  satfdmlem  35336  satf0op  35345  fmlasuc  35354  dfrdg4  35915  altopthsn  35925  btwncomim  35977  btwnexch3  35984  btwnexch2  35987  endofsegid  36049  opnrebl2  36287  nn0prpwlem  36288  onsuct0  36407  ordcmp  36413  nndivsub  36423  dnibndlem13  36456  bj-cbval  36615  bj-cbvex  36616  bj-cbvexw  36642  bj-cbv3tb  36753  bj-spimtv  36760  bj-equsal  36792  bj-sbsb  36803  bj-vtoclf  36881  bj-zfauscl  36890  bj-gabss  36901  bj-gabeqd  36903  currysetlem2  36914  bj-snsetex  36929  bj-ismooredr2  37076  bj-inftyexpiinj  37175  bj-finsumval0  37251  bj-fvimacnv0  37252  bj-bary1lem1  37277  bj-bary1  37278  f1omptsnlem  37302  iooelexlt  37328  relowlpssretop  37330  rdgeqoa  37336  finxpsuclem  37363  fvineqsneq  37378  pibt2  37383  wl-equsal1i  37498  wl-ax11-lem10  37548  ltflcei  37568  sin2h  37570  cos2h  37571  tan2h  37572  lindsenlbs  37575  matunitlindf  37578  poimirlem3  37583  poimirlem4  37584  poimirlem18  37598  poimirlem20  37600  poimirlem21  37601  poimirlem22  37602  poimirlem24  37604  poimirlem25  37605  poimirlem26  37606  poimirlem27  37607  poimirlem28  37608  poimirlem31  37611  poimir  37613  heicant  37615  mblfinlem1  37617  mblfinlem2  37618  mblfinlem3  37619  mblfinlem4  37620  mbfresfi  37626  cnambfre  37628  ftc1anc  37661  dvasin  37664  areacirclem1  37668  areacirclem4  37671  areacirc  37673  brabg2  37677  fzmul  37701  fdc  37705  incsequz2  37709  isbnd2  37743  opidonOLD  37812  opidon2OLD  37814  grpomndo  37835  elghomlem2OLD  37846  rngoueqz  37900  dvrunz  37914  divrngidl  37988  refressn  38399  dral1-o  38860  lsatn0  38955  l1cvpat  39010  leat2  39250  atnle  39273  cvlcvr1  39295  cvrexchlem  39376  cvratlem  39378  cvrat  39379  atcvrj0  39385  atle  39393  snatpsubN  39707  linepsubN  39709  pmapsub  39725  lneq2at  39735  lncvrelatN  39738  2llnma3r  39745  cdlemblem  39750  paddasslem5  39781  poml4N  39910  lhpmcvr4N  39983  trlval2  40120  cdlemd6  40160  cdleme7ga  40205  cdleme25b  40311  cdleme29b  40332  cdleme35fnpq  40406  cdleme50f1  40500  cdlemf1  40518  cdlemg27b  40653  cdlemk28-3  40865  tendospcanN  40980  diaf11N  41006  dia2dimlem1  41021  dibf11N  41118  dihf11  41224  dihmeetlem1N  41247  dochvalr  41314  dochnel2  41349  dvh4dimlem  41400  dochsat0  41414  mapd1o  41605  hdmapf1oN  41822  hgmapval0  41849  hgmapf1oN  41860  hlhilhillem  41921  nnproddivdvdsd  41957  lcmineqlem  42009  aks4d1p1p5  42032  aks4d1p3  42035  aks4d1p8d2  42042  aks4d1p8  42044  aks4d1p9  42045  fldhmf1  42047  isprimroot2  42051  primrootsunit1  42054  primrootscoprmpow  42056  posbezout  42057  primrootscoprbij  42059  primrootlekpowne0  42062  primrootspoweq0  42063  aks6d1c1p1  42064  aks6d1c1p2  42066  aks6d1c1p3  42067  aks6d1c1p4  42068  aks6d1c1p5  42069  aks6d1c1p7  42070  aks6d1c1p6  42071  aks6d1c1p8  42072  aks6d1c2p2  42076  aks6d1c2lem3  42083  aks6d1c2lem4  42084  hashnexinj  42085  hashnexinjle  42086  aks6d1c2  42087  aks6d1c5lem0  42092  aks6d1c5lem1  42093  aks6d1c5  42096  sticksstones1  42103  sticksstones3  42105  sticksstones8  42110  sticksstones11  42113  sticksstones12  42115  sticksstones20  42123  sticksstones22  42125  aks6d1c6lem3  42129  aks6d1c6lem4  42130  aks6d1c6isolem1  42131  aks6d1c6isolem2  42132  aks6d1c6lem5  42134  aks6d1c7  42141  rhmqusspan  42142  unitscyglem2  42153  unitscyglem3  42154  aks5lem8  42158  metakunt7  42168  sn-axprlem3  42210  oexpreposd  42309  frlmsnic  42495  fsuppind  42545  prjspval  42558  rexrabdioph  42750  fphpdo  42773  irrapxlem3  42780  rmxypairf1o  42868  rmxycomplete  42874  zindbi  42903  lermxnn0  42907  ltrmy  42909  rmyeq0  42910  rmyeq  42911  lermy  42912  acongsym  42933  acongneg2  42934  wepwsolem  42999  onsupuni  43190  onsupmaxb  43200  onsucf1o  43234  onov0suclim  43236  oe0suclim  43239  onsucwordi  43250  cantnfresb  43286  omabs2  43294  tfsconcat0b  43308  tfsconcatrev  43310  naddcnffo  43326  oaun3lem1  43336  oaltom  43367  omltoe  43369  sdomne0  43375  sdomne0d  43376  safesnsupfidom1o  43379  intabssd  43481  iscard4  43495  ss2iundf  43621  frege129d  43725  frege133d  43727  axfrege52a  43818  axfrege52c  43849  ntrk0kbimka  44001  gneispace  44096  suprleubrd  44128  suprlubrd  44130  radcnvrat  44283  nzss  44286  expgrowthi  44302  ordpss  44420  bi23impib  44456  bi23imp13  44462  rspsbc2  44505  tratrb  44507  sbcim2g  44509  truniALT  44512  3impcombi  44788  tpid3gVD  44813  orbi1rVD  44819  sbc3orgVD  44822  rspsbc2VD  44826  tratrbVD  44832  sbcim2gVD  44846  sbcbiVD  44847  truniALTVD  44849  trintALTVD  44851  trintALT  44852  csbingVD  44855  csbsngVD  44864  csbxpgVD  44865  csbresgVD  44866  csbrngVD  44867  csbima12gALTVD  44868  csbunigVD  44869  csbfv12gALTVD  44870  relopabVD  44872  isosctrlem1ALT  44905  fzisoeu  45215  xrralrecnnge  45305  allbutfi  45308  climinf  45527  liminfreuzlem  45723  climliminf  45727  climliminflimsup  45729  xlimpnfxnegmnf  45735  xlimbr  45748  stoweidlem7  45928  stoweidlem62  45983  sge0gerpmpt  46323  meaiuninclem  46401  carageniuncllem2  46443  issmflem  46648  et-sqrtnegnre  46794  natlocalincr  46795  tworepnotupword  46805  funressnfv  46958  funressnvmo  46960  f1cof1b  46992  2reu3  47025  ralbinrald  47037  afv0fv0  47064  afv0nbfvbi  47066  afvfv0bi  47067  fnbrafvb  47069  afvres  47087  tz6.12-afv  47088  afvco2  47091  ndmaovcl  47118  afv2res  47154  tz6.12-afv2  47155  nelbrim  47190  f1oresf1o2  47206  zm1nn  47217  nltle2tri  47228  subsubelfzo0  47241  iccpartres  47292  iccpartiltu  47296  fargshiftfv  47313  ichnreuop  47346  ichreuopeq  47347  prsprel  47361  sprsymrelf1lem  47365  sprsymrelfolem2  47367  sprsymrelfo  47371  prpair  47375  paireqne  47385  sbcpr  47395  fmtnof1  47409  goldbachthlem2  47420  fmtnoprmfac1  47439  fmtnoprmfac2  47441  lighneallem2  47480  lighneallem4b  47483  lighneallem4  47484  evennodd  47517  oddneven  47518  oexpnegnz  47552  evenltle  47591  fpprwppr  47613  fpprwpprb  47614  gbowge7  47637  gbege6  47639  sbgoldbwt  47651  sbgoldbst  47652  nnsum3primesle9  47668  bgoldbtbndlem2  47680  grimprop  47753  isuspgrimlem  47758  uhgrimisgrgriclem  47782  clnbgrgrimlem  47785  grtriproplem  47790  isgrtri  47794  grimgrtri  47798  grlimprop  47808  uspgrlimlem2  47813  uspgrlimlem3  47814  clintop  47931  isassintop  47933  lidldomn1  47954  uzlidlring  47958  2zrngnmlid2  47980  rngccatidALTV  47995  ringccatidALTV  48029  srhmsubcALTV  48048  ztprmneprm  48072  pgrpgt2nabl  48091  lindslinindimp2lem4  48190  lincresunit3  48210  fldivexpfllog2  48299  digexp  48341  naryfvalelfv  48366  affinecomb1  48436  eenglngeehlnmlem1  48471  eenglngeehlnmlem2  48472  eenglngeehlnm  48473  itscnhlc0yqe  48493  itsclc0yqsol  48498  itscnhlc0xyqsol  48499  itschlc0xyqsol1  48500  itschlc0xyqsol  48501  itsclquadeu  48511  inlinecirc02plem  48520  inlinecirc02p  48521  pm4.71da  48523  mofsn  48557  seposep  48605  idmon  48683  idepi  48684  prsthinc  48721  grptcmon  48763  grptcepi  48764  spd  48770  spcdvw  48771  setrec2fun  48784