Theorem biimpd 228

Description: Deduce an implication from a logical equivalence. Deduction associated with biimp 214 and biimpi 215. (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 214	. 2 ⊢ ((𝜓 ↔ 𝜒) → (𝜓 → 𝜒))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝜓 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  mpbid  231  sylibd  238  sylbid  239  mpbidi  240  syl5ib  243  syl6bi  252  con4bid  317  mtbird  325  mtbiri  327  imbi1d  342  bitr3  353  pm5.21im  375  biimpa  477  alexbii  1836  spvv  2001  spfw  2037  cbvalw  2039  alcomiwOLD  2048  sbequi  2088  chvarfv  2234  cbvalv1  2339  spv  2394  chvar  2396  cbval  2399  sb1  2480  nfsb4t  2504  exmoeu  2582  euim  2620  2eu3  2656  eqrdav  2738  rgen2a  3159  ralbida  3160  ralcom2  3291  raleleq  3357  ceqsalgALT  3466  vtoclf  3498  spcdv  3534  rspcdv  3554  rspcebdv  3556  rexraleqim  3578  elabgtOLD  3605  sbcn1  3772  sbcim1OLD  3774  sbcbi1  3778  sbeqalb  3785  sbcel21v  3790  disj  4382  elpwunsn  4620  rabsnifsb  4659  ssunsn2  4761  preqr1g  4784  iuneqconst  4936  axprlem3  5349  sbcop1  5403  propeqop  5422  euotd  5428  rexopabb  5442  sotr2  5536  relop  5762  elinxp  5932  elimasni  6002  sotri2  6039  onmindif  6359  iotaval  6411  dffv2  6872  mpteqb  6903  elfvmptrab  6912  chfnrn  6935  elpreima  6944  iinpreima  6955  exfo  6990  ffnfv  7001  f1elima  7145  f1eqcocnv  7182  f1eqcocnvOLD  7183  fliftfun  7192  soisores  7207  isotr  7216  isomin  7217  ovmpodv2  7440  difsnexi  7620  onint  7649  oneqmin  7659  ordunisuc2  7700  tfindsg  7716  findsg  7755  f1oweALT  7824  el2mpocl  7935  ressuppss  8008  funsssuppss  8015  suppofssd  8028  smoiso  8202  seqomlem2  8291  oaordi  8386  oawordri  8390  oaordex  8398  oalimcl  8400  omwordi  8411  oewordi  8431  oelim2  8435  nnmwordi  8475  xpider  8586  iiner  8587  undifixp  8731  mptelixpg  8732  dom2lem  8789  findcard2s  8957  pssnn  8960  nneneq  9001  nneneqOLD  9013  fineqvlem  9046  pssnnOLD  9049  dif1enALT  9059  unfilem2  9088  xpfi  9094  domunfican  9096  f1dmvrnfibi  9112  fsuppimp  9143  dffi2  9191  infsupprpr  9272  wemaplem2  9315  suc11reg  9386  noinfep  9427  cantnflem1  9456  r1fin  9540  tcrank  9651  cardlim  9739  pr2nelem  9769  fseqenlem1  9789  alephnbtwn  9836  alephord2i  9842  alephf1  9850  cardaleph  9854  alephiso  9863  dfac12lem2  9909  ackbij1lem16  10000  cflm  10015  cfcoflem  10037  sornom  10042  fin23lem27  10093  isf32lem7  10124  fin17  10159  fin1a2lem2  10166  fin1a2lem4  10168  fin1a2lem6  10170  fin1a2lem9  10173  axdc3lem2  10216  zorn2lem7  10267  uniimadom  10309  inar1  10540  grothomex  10594  addcanpi  10664  mulcanpi  10665  enqer  10686  genpcd  10771  genpnmax  10772  ltexprlem4  10804  reclem3pr  10814  reclem4pr  10815  suplem2pr  10818  axpre-ltadd  10932  axpre-sup  10934  ltletr  11076  00id  11159  addn0nid  11404  mul0or  11624  prodgt02  11832  lemul1a  11838  mulgt1  11843  divgt0  11852  divge0  11853  ledivp1i  11909  ltdivp1i  11910  cju  11978  nnsub  12026  nominpos  12219  nn0n0n1ge2  12309  btwnnz  12405  suprfinzcl  12445  ublbneg  12682  zmax  12694  cnref1o  12734  ltsubrp  12775  ltaddrp  12776  xrltletr  12900  qbtwnre  12942  xltnegi  12959  xnn0xadd0  12990  iccsupr  13183  icoshft  13214  difreicc  13225  iccshftri  13228  iccshftli  13230  iccdili  13232  icccntri  13234  fzen  13282  elfz1b  13334  fzofzim  13443  eluzgtdifelfzo  13458  elfzo1elm1fzo0  13497  injresinjlem  13516  injresinj  13517  flval2  13543  flval3  13544  modmuladdim  13643  modaddmodup  13663  addmodlteq  13675  fseqsupubi  13707  ssnn0fi  13714  mptnn0fsuppr  13728  sq01  13949  hashf1rn  14076  hashgt12el  14146  hashgt12el2  14147  hash2pr  14192  hash2exprb  14194  hashge2el2difr  14204  hashtpg  14208  hash3tr  14213  lswlgt0cl  14281  ccatalpha  14307  pfxfv  14404  pfxsuff1eqwrdeq  14421  ccatopth2  14439  swrdccat  14457  swrdccat3blem  14461  reuccatpfxs1lem  14468  repsdf2  14500  repswsymball  14501  repswrevw  14509  cshweqrep  14543  cshw1  14544  2cshwcshw  14547  scshwfzeqfzo  14548  cshwcsh2id  14550  swrdco  14559  swrd2lsw  14674  2swrd2eqwrdeq  14675  wwlktovfo  14682  cjre  14859  icodiamlt  15156  reusq0  15183  o1lo1  15255  o1of2  15331  o1rlimmul  15337  zsum  15439  modfsummods  15514  zprod  15656  reeff1  15838  dvdsmod0  15978  dvds2lem  15987  muldvds1  15999  dvdscmulr  16003  dvdsmulcr  16004  dvdsdivcl  16034  mod2eq1n2dvds  16065  oddnn02np1  16066  divalglem8  16118  ndvdsadd  16128  zeqzmulgcd  16226  dfgcd2  16263  gcdmultipleOLD  16269  absproddvds  16331  lcmftp  16350  coprmdvds  16367  2mulprm  16407  isprm5  16421  divgcdodd  16424  isprm6  16428  prmdvdsexpr  16431  cncongrprm  16442  phiprmpw  16486  modprm0  16515  pythagtriplem4  16529  pcz  16591  difsqpwdvds  16597  1arith  16637  prmgaplem5  16765  prmgaplem6  16766  cshwrepswhash1  16813  divsfval  17267  catsubcat  17563  fthmon  17652  isinitoi  17723  istermoi  17724  iszeroi  17733  setcmon  17811  setcepi  17812  funcestrcsetclem8  17873  fthestrcsetc  17876  funcsetcestrclem8  17888  fthsetcestrc  17891  odupos  18055  pltnle  18065  pltval3  18066  lublecllem  18087  latasym  18170  mrelatglb  18287  mrelatlub  18289  cnvpsb  18306  isgrpid2  18625  ghmghmrn  18862  ghmf1  18872  orbsta  18928  resscntz  18947  gsmsymgrfixlem1  19044  gsmsymgreqlem2  19048  mndodcongi  19160  odf1  19178  lsmss1  19280  lsmss2  19282  efgredeu  19367  cntzcmnss  19451  lt6abl  19505  ablfaclem3  19699  ringinvnz1ne0  19840  kerf1ghm  19996  lspsneq  20393  lspsneu  20394  lsmcv  20412  lidldvgen  20535  0ringnnzr  20549  domnmuln0  20578  opprdomn  20581  domnchr  20745  znf1o  20768  zntoslem  20773  znfld  20777  cygznlem2a  20784  cygznlem3  20786  phlssphl  20873  islindf4  21054  uvcendim  21063  ply1scln0  21471  gsummoncoe1  21484  matvscl  21589  scmataddcl  21674  scmatsubcl  21675  scmatfo  21688  scmatghm  21691  maducoeval2  21798  slesolinv  21838  cramerimplem2  21842  cpmatelimp  21870  cpmatelimp2  21872  cpmatacl  21874  cpmatinvcl  21875  pm2mpf1  21957  cayhamlem1  22024  cayleyhamilton1  22050  0ntr  22231  islpi  22309  lmss  22458  cmpcld  22562  cmpfi  22568  1stcelcls  22621  comppfsc  22692  ptcnplem  22781  qtophmeo  22977  fbdmn0  22994  fbasrn  23044  elfm3  23110  fmfnfmlem4  23117  fclscf  23185  cnpfcf  23201  alexsubALTlem3  23209  tsmsres  23304  blval2  23727  tnggrpr  23828  nmoleub  23904  nmhmcn  24292  ncvs1  24330  iscau4  24452  caussi  24470  cmssmscld  24523  cmslssbn  24545  cniccbdd  24634  ovoliunnul  24680  mbfinf  24838  itg2splitlem  24922  dvcn  25094  c1lip1  25170  c1lip3  25172  dvcnvrelem1  25190  ply1divex  25310  quotcan  25478  aannenlem1  25497  taylf  25529  ulmcaulem  25562  ulmcau  25563  reeff1o  25615  logccv  25827  logreclem  25921  isosctrlem2  25978  xrlimcnp  26127  rlimcxp  26132  ftalem7  26237  vmappw  26274  fsumvma  26370  dchreq  26415  dchrptlem1  26421  dchrsum  26426  bposlem7  26447  lgsqrlem2  26504  lgsdchr  26512  gausslemma2dlem1a  26522  lgseisenlem2  26533  lgsquad2  26543  2lgslem1b  26549  2sqlem6  26580  2sqnn0  26595  addsq2reu  26597  2sqreulem2  26609  tgcgrcomimp  26847  isperp2  27085  xmstrkgc  27262  brbtwn  27276  brcgr  27277  axcgrid  27293  axeuclidlem  27339  axeuclid  27340  elntg2  27362  lpvtx  27447  upgrex  27471  upgrpredgv  27518  upgredgpr  27521  uhgr0v0e  27614  subgrprop  27649  fusgrfisbase  27704  edgnbusgreu  27743  nbusgredgeu0  27744  cusgredg  27800  structtocusgr  27822  cusgrsize2inds  27829  cusgrsize  27830  usgredgsscusgredg  27835  fusgrmaxsize  27840  uspgrloopvtxel  27892  umgr2v2e  27901  vtxdginducedm1fi  27920  finsumvtxdg2sstep  27925  rgrprop  27936  rusgrprop  27938  0uhgrrusgr  27954  rusgrpropedg  27960  ewlkprop  27979  upgrewlkle2  27982  wlkprop  27987  upgrwlkcompim  28019  uspgr2wlkeq  28022  wlklenvclwlk  28031  wlklenvclwlkOLD  28032  wlkonprop  28035  wlkres  28047  redwlk  28049  wlkdlem2  28060  wksonproplem  28081  wksonproplemOLD  28082  usgr2trlspth  28138  usgr2pth  28141  pthdlem1  28143  crctcshwlkn0lem4  28187  wwlksnprcl  28213  wlkiswwlks2  28249  wwlksm1edg  28255  wlknewwlksn  28261  wwlksnred  28266  wwlksnextbi  28268  wwlksnextwrd  28271  wwlksnextinj  28273  wwlksnextsurj  28274  umgr2wlk  28323  umgrwwlks2on  28331  elwwlks2  28340  clwwlk1loop  28361  umgrclwwlkge2  28364  clwlkclwwlklem2a1  28365  clwlkclwwlklem2a4  28370  clwlkclwwlklem2a  28371  clwlkclwwlklem2  28373  clwlkclwwlkfo  28382  clwwisshclwwslemlem  28386  clwwlknwwlksn  28411  clwwlknlbonbgr1  28412  clwwlkn1loopb  28416  clwwlkf  28420  clwwlknon1  28470  clwwlknonwwlknonb  28479  clwwlknonex2lem2  28481  vdn0conngrumgrv2  28569  frgrnbnb  28666  frgrncvvdeqlem2  28673  frgrncvvdeqlem3  28674  frgrncvvdeqlem6  28677  frgrwopreglem4a  28683  fusgr2wsp2nb  28707  frrusgrord0lem  28712  numclwwlk2lem1lem  28715  2clwwlk2clwwlklem  28719  2clwwlk2clwwlk  28723  numclwwlk1lem2foa  28727  numclwwlk1lem2f1  28730  frgrreg  28767  hlipgt0  29285  ocin  29667  ocnel  29669  shmodsi  29760  pjmf1  30087  unopf1o  30287  staddi  30617  stadd3i  30619  mdi  30666  dmdmd  30671  dmdi  30673  dmdbr2  30674  dmdbr3  30676  dmdbr4  30677  dmdi4  30678  mdsl1i  30692  superpos  30725  cvbr4i  30738  atssma  30749  atcv1  30751  atomli  30753  chirredlem1  30761  addltmulALT  30817  bian1d  30818  ifeqeqx  30894  disjxpin  30936  suppss3  31068  fpwrelmap  31077  prmdvdsbc  31139  ogrpaddlt  31352  metider  31853  tpr2rico  31871  xrge0iifiso  31894  qqhcn  31950  qqhucn  31951  esumlub  32037  esumpinfval  32050  esumpinfsum  32054  ballotlemfc0  32468  ballotlemfcc  32469  ftc2re  32587  bnj517  32874  fnrelpredd  33070  hashfundm  33083  pfxwlk  33094  subgrwlk  33103  loop1cycl  33108  erdsze2lem2  33175  satfv1  33334  satfdmlem  33339  satf0op  33348  fmlasuc  33357  poseq  33811  soseq  33812  sltval2  33868  sltres  33874  nodenselem8  33903  nodense  33904  noresle  33909  scutun12  34013  madeval2  34046  elmade  34060  dfrdg4  34262  altopthsn  34272  btwncomim  34324  btwnexch3  34331  btwnexch2  34334  endofsegid  34396  opnrebl2  34519  nn0prpwlem  34520  onsuct0  34639  ordcmp  34645  nndivsub  34655  dnibndlem13  34679  bj-cbval  34839  bj-cbvex  34840  bj-cbvexw  34866  bj-cbv3tb  34978  bj-spimtv  34985  bj-equsal  35018  bj-sbsb  35029  bj-vtoclf  35109  bj-zfauscl  35121  bj-gabss  35132  bj-gabeqd  35134  currysetlem2  35146  bj-snsetex  35162  bj-ismooredr2  35290  bj-inftyexpiinj  35389  bj-finsumval0  35465  bj-fvimacnv0  35466  bj-bary1lem1  35491  bj-bary1  35492  f1omptsnlem  35516  iooelexlt  35542  relowlpssretop  35544  rdgeqoa  35550  finxpsuclem  35577  fvineqsneq  35592  pibt2  35597  wl-equsal1i  35711  wl-ax11-lem10  35754  ltflcei  35774  sin2h  35776  cos2h  35777  tan2h  35778  lindsenlbs  35781  matunitlindf  35784  poimirlem3  35789  poimirlem4  35790  poimirlem18  35804  poimirlem20  35806  poimirlem21  35807  poimirlem22  35808  poimirlem24  35810  poimirlem25  35811  poimirlem26  35812  poimirlem27  35813  poimirlem28  35814  poimirlem31  35817  poimir  35819  heicant  35821  mblfinlem1  35823  mblfinlem2  35824  mblfinlem3  35825  mblfinlem4  35826  mbfresfi  35832  cnambfre  35834  ftc1anc  35867  dvasin  35870  areacirclem1  35874  areacirclem4  35877  areacirc  35879  brabg2  35883  fzmul  35908  fdc  35912  incsequz2  35916  isbnd2  35950  opidonOLD  36019  opidon2OLD  36021  grpomndo  36042  elghomlem2OLD  36053  rngoueqz  36107  dvrunz  36121  divrngidl  36195  dral1-o  36925  lsatn0  37020  l1cvpat  37075  leat2  37315  atnle  37338  cvlcvr1  37360  cvrexchlem  37440  cvratlem  37442  cvrat  37443  atcvrj0  37449  atle  37457  snatpsubN  37771  linepsubN  37773  pmapsub  37789  lneq2at  37799  lncvrelatN  37802  2llnma3r  37809  cdlemblem  37814  paddasslem5  37845  poml4N  37974  lhpmcvr4N  38047  trlval2  38184  cdlemd6  38224  cdleme7ga  38269  cdleme25b  38375  cdleme29b  38396  cdleme35fnpq  38470  cdleme50f1  38564  cdlemf1  38582  cdlemg27b  38717  cdlemk28-3  38929  tendospcanN  39044  diaf11N  39070  dia2dimlem1  39085  dibf11N  39182  dihf11  39288  dihmeetlem1N  39311  dochvalr  39378  dochnel2  39413  dvh4dimlem  39464  dochsat0  39478  mapd1o  39669  hdmapf1oN  39886  hgmapval0  39913  hgmapf1oN  39924  hlhilhillem  39985  nnproddivdvdsd  40016  lcmineqlem  40067  aks4d1p1p5  40090  aks4d1p3  40093  aks4d1p8d2  40100  aks4d1p8  40102  aks4d1p9  40103  sticksstones1  40109  sticksstones3  40111  sticksstones8  40116  sticksstones11  40119  sticksstones12  40121  sticksstones20  40129  sticksstones22  40131  metakunt7  40138  sn-axprlem3  40193  frlmsnic  40270  fsuppind  40286  oexpreposd  40328  rtprmirr  40354  prjspval  40449  rexrabdioph  40623  fphpdo  40646  irrapxlem3  40653  rmxypairf1o  40740  rmxycomplete  40746  zindbi  40775  lermxnn0  40779  ltrmy  40781  rmyeq0  40782  rmyeq  40783  lermy  40784  acongsym  40805  acongneg2  40806  wepwsolem  40874  intabssd  41133  iscard4  41147  ss2iundf  41274  frege129d  41378  frege133d  41380  axfrege52a  41471  axfrege52c  41502  ntrk0kbimka  41656  gneispace  41751  suprleubrd  41784  suprlubrd  41786  radcnvrat  41939  nzss  41942  expgrowthi  41958  ordpss  42076  bi23impib  42112  bi23imp13  42118  rspsbc2  42161  tratrb  42163  sbcim2g  42165  truniALT  42168  3impcombi  42444  tpid3gVD  42469  orbi1rVD  42475  sbc3orgVD  42478  rspsbc2VD  42482  tratrbVD  42488  sbcim2gVD  42502  sbcbiVD  42503  truniALTVD  42505  trintALTVD  42507  trintALT  42508  csbingVD  42511  csbsngVD  42520  csbxpgVD  42521  csbresgVD  42522  csbrngVD  42523  csbima12gALTVD  42524  csbunigVD  42525  csbfv12gALTVD  42526  relopabVD  42528  isosctrlem1ALT  42561  fzisoeu  42846  xrralrecnnge  42937  allbutfi  42940  climinf  43154  liminfreuzlem  43350  climliminf  43354  climliminflimsup  43356  xlimpnfxnegmnf  43362  xlimbr  43375  stoweidlem7  43555  stoweidlem62  43610  sge0gerpmpt  43947  meaiuninclem  44025  carageniuncllem2  44067  issmflem  44272  funressnfv  44548  funressnvmo  44550  f1cof1b  44580  2reu3  44613  ralbinrald  44625  afv0fv0  44652  afv0nbfvbi  44654  afvfv0bi  44655  fnbrafvb  44657  afvres  44675  tz6.12-afv  44676  afvco2  44679  ndmaovcl  44706  afv2res  44742  tz6.12-afv2  44743  nelbrim  44778  f1oresf1o2  44794  zm1nn  44805  nltle2tri  44816  subsubelfzo0  44829  iccpartres  44881  iccpartiltu  44885  fargshiftfv  44902  ichnreuop  44935  ichreuopeq  44936  prsprel  44950  sprsymrelf1lem  44954  sprsymrelfolem2  44956  sprsymrelfo  44960  prpair  44964  paireqne  44974  sbcpr  44984  fmtnof1  44998  goldbachthlem2  45009  fmtnoprmfac1  45028  fmtnoprmfac2  45030  lighneallem2  45069  lighneallem4b  45072  lighneallem4  45073  evennodd  45106  oddneven  45107  oexpnegnz  45141  evenltle  45180  fpprwppr  45202  fpprwpprb  45203  gbowge7  45226  gbege6  45228  sbgoldbwt  45240  sbgoldbst  45241  nnsum3primesle9  45257  bgoldbtbndlem2  45269  isomuspgrlem1  45290  isomuspgrlem2b  45292  isomuspgrlem2c  45293  isomuspgrlem2d  45294  mgmpropd  45340  clintop  45413  isassintop  45415  lidldomn1  45490  uzlidlring  45498  2zrngnmlid2  45520  rngccatidALTV  45558  ringccatidALTV  45621  srhmsubc  45645  srhmsubcALTV  45663  ztprmneprm  45694  pgrpgt2nabl  45713  lindslinindimp2lem4  45813  lincresunit3  45833  fldivexpfllog2  45922  digexp  45964  naryfvalelfv  45989  affinecomb1  46059  eenglngeehlnmlem1  46094  eenglngeehlnmlem2  46095  eenglngeehlnm  46096  itscnhlc0yqe  46116  itsclc0yqsol  46121  itscnhlc0xyqsol  46122  itschlc0xyqsol1  46123  itschlc0xyqsol  46124  itsclquadeu  46134  inlinecirc02plem  46143  inlinecirc02p  46144  pm4.71da  46146  mofsn  46182  seposep  46230  idmon  46308  idepi  46309  prsthinc  46346  grptcmon  46388  grptcepi  46389  spd  46395  spcdvw  46396  setrec2fun  46409  natlocalincr  46522  tworepnotupword  46532