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  316  mtbird  324  mtbiri  326  imbi1d  341  bitr3  352  pm5.21im  374  biimpa  476  alexbii  1836  spvv  2001  spfw  2037  cbvalw  2039  alcomiwOLD  2048  sbequi  2088  chvarfv  2236  cbvalv1  2340  spv  2393  chvar  2395  cbval  2398  sb1  2479  nfsb4t  2503  exmoeu  2581  euim  2619  2eu3  2655  eqrdav  2737  rgen2a  3155  ralbida  3156  ralcom2  3288  raleleq  3347  ceqsalgALT  3455  vtoclf  3487  spcdv  3523  rspcdv  3543  rspcebdv  3545  rexraleqim  3569  elabgtOLD  3597  sbcn1  3766  sbcim1OLD  3768  sbcbi1  3773  sbeqalb  3780  sbcel21v  3785  disj  4378  elpwunsn  4616  rabsnifsb  4655  ssunsn2  4757  preqr1g  4780  iuneqconst  4932  axprlem3  5343  sbcop1  5396  propeqop  5415  euotd  5421  rexopabb  5434  sotr2  5526  relop  5748  elinxp  5918  elimasni  5988  sotri2  6023  onmindif  6340  iotaval  6392  dffv2  6845  mpteqb  6876  elfvmptrab  6885  chfnrn  6908  elpreima  6917  iinpreima  6928  exfo  6963  ffnfv  6974  f1elima  7117  f1eqcocnv  7153  f1eqcocnvOLD  7154  fliftfun  7163  soisores  7178  isotr  7187  isomin  7188  ovmpodv2  7409  difsnexi  7589  onint  7617  oneqmin  7627  ordunisuc2  7666  tfindsg  7682  findsg  7720  f1oweALT  7788  el2mpocl  7897  ressuppss  7970  funsssuppss  7977  suppofssd  7990  smoiso  8164  seqomlem2  8252  oaordi  8339  oawordri  8343  oaordex  8351  oalimcl  8353  omwordi  8364  oewordi  8384  oelim2  8388  nnmwordi  8428  xpider  8535  iiner  8536  undifixp  8680  mptelixpg  8681  dom2lem  8735  nneneq  8896  findcard2s  8910  pssnn  8913  fineqvlem  8966  pssnnOLD  8969  dif1enALT  8980  unfilem2  9009  xpfi  9015  domunfican  9017  f1dmvrnfibi  9033  fsuppimp  9064  dffi2  9112  infsupprpr  9193  wemaplem2  9236  suc11reg  9307  noinfep  9348  cantnflem1  9377  trpredrec  9415  r1fin  9462  tcrank  9573  cardlim  9661  pr2nelem  9691  fseqenlem1  9711  alephnbtwn  9758  alephord2i  9764  alephf1  9772  cardaleph  9776  alephiso  9785  dfac12lem2  9831  ackbij1lem16  9922  cflm  9937  cfcoflem  9959  sornom  9964  fin23lem27  10015  isf32lem7  10046  fin17  10081  fin1a2lem2  10088  fin1a2lem4  10090  fin1a2lem6  10092  fin1a2lem9  10095  axdc3lem2  10138  zorn2lem7  10189  uniimadom  10231  inar1  10462  grothomex  10516  addcanpi  10586  mulcanpi  10587  enqer  10608  genpcd  10693  genpnmax  10694  ltexprlem4  10726  reclem3pr  10736  reclem4pr  10737  suplem2pr  10740  axpre-ltadd  10854  axpre-sup  10856  ltletr  10997  00id  11080  addn0nid  11325  mul0or  11545  prodgt02  11753  lemul1a  11759  mulgt1  11764  divgt0  11773  divge0  11774  ledivp1i  11830  ltdivp1i  11831  cju  11899  nnsub  11947  nominpos  12140  nn0n0n1ge2  12230  btwnnz  12326  suprfinzcl  12365  ublbneg  12602  zmax  12614  cnref1o  12654  ltsubrp  12695  ltaddrp  12696  xrltletr  12820  qbtwnre  12862  xltnegi  12879  xnn0xadd0  12910  iccsupr  13103  icoshft  13134  difreicc  13145  iccshftri  13148  iccshftli  13150  iccdili  13152  icccntri  13154  fzen  13202  elfz1b  13254  fzofzim  13362  eluzgtdifelfzo  13377  elfzo1elm1fzo0  13416  injresinjlem  13435  injresinj  13436  flval2  13462  flval3  13463  modmuladdim  13562  modaddmodup  13582  addmodlteq  13594  fseqsupubi  13626  ssnn0fi  13633  mptnn0fsuppr  13647  sq01  13868  hashf1rn  13995  hashgt12el  14065  hashgt12el2  14066  hash2pr  14111  hash2exprb  14113  hashge2el2difr  14123  hashtpg  14127  hash3tr  14132  lswlgt0cl  14200  ccatalpha  14226  pfxfv  14323  pfxsuff1eqwrdeq  14340  ccatopth2  14358  swrdccat  14376  swrdccat3blem  14380  reuccatpfxs1lem  14387  repsdf2  14419  repswsymball  14420  repswrevw  14428  cshweqrep  14462  cshw1  14463  2cshwcshw  14466  scshwfzeqfzo  14467  cshwcsh2id  14469  swrdco  14478  swrd2lsw  14593  2swrd2eqwrdeq  14594  wwlktovfo  14601  cjre  14778  icodiamlt  15075  reusq0  15102  o1lo1  15174  o1of2  15250  o1rlimmul  15256  zsum  15358  modfsummods  15433  zprod  15575  reeff1  15757  dvdsmod0  15897  dvds2lem  15906  muldvds1  15918  dvdscmulr  15922  dvdsmulcr  15923  dvdsdivcl  15953  mod2eq1n2dvds  15984  oddnn02np1  15985  divalglem8  16037  ndvdsadd  16047  zeqzmulgcd  16145  dfgcd2  16182  gcdmultipleOLD  16188  absproddvds  16250  lcmftp  16269  coprmdvds  16286  2mulprm  16326  isprm5  16340  divgcdodd  16343  isprm6  16347  prmdvdsexpr  16350  cncongrprm  16361  phiprmpw  16405  modprm0  16434  pythagtriplem4  16448  pcz  16510  difsqpwdvds  16516  1arith  16556  prmgaplem5  16684  prmgaplem6  16685  cshwrepswhash1  16732  divsfval  17175  catsubcat  17470  fthmon  17559  isinitoi  17630  istermoi  17631  iszeroi  17640  setcmon  17718  setcepi  17719  funcestrcsetclem8  17780  fthestrcsetc  17783  funcsetcestrclem8  17795  fthsetcestrc  17798  odupos  17961  pltnle  17971  pltval3  17972  lublecllem  17993  latasym  18076  mrelatglb  18193  mrelatlub  18195  cnvpsb  18212  isgrpid2  18531  ghmghmrn  18768  ghmf1  18778  orbsta  18834  resscntz  18853  gsmsymgrfixlem1  18950  gsmsymgreqlem2  18954  mndodcongi  19066  odf1  19084  lsmss1  19186  lsmss2  19188  efgredeu  19273  cntzcmnss  19357  lt6abl  19411  ablfaclem3  19605  ringinvnz1ne0  19746  kerf1ghm  19902  lspsneq  20299  lspsneu  20300  lsmcv  20318  lidldvgen  20439  0ringnnzr  20453  domnmuln0  20482  opprdomn  20485  domnchr  20648  znf1o  20671  zntoslem  20676  znfld  20680  cygznlem2a  20687  cygznlem3  20689  phlssphl  20776  islindf4  20955  uvcendim  20964  ply1scln0  21372  gsummoncoe1  21385  matvscl  21488  scmataddcl  21573  scmatsubcl  21574  scmatfo  21587  scmatghm  21590  maducoeval2  21697  slesolinv  21737  cramerimplem2  21741  cpmatelimp  21769  cpmatelimp2  21771  cpmatacl  21773  cpmatinvcl  21774  pm2mpf1  21856  cayhamlem1  21923  cayleyhamilton1  21949  0ntr  22130  islpi  22208  lmss  22357  cmpcld  22461  cmpfi  22467  1stcelcls  22520  comppfsc  22591  ptcnplem  22680  qtophmeo  22876  fbdmn0  22893  fbasrn  22943  elfm3  23009  fmfnfmlem4  23016  fclscf  23084  cnpfcf  23100  alexsubALTlem3  23108  tsmsres  23203  blval2  23624  tnggrpr  23725  nmoleub  23801  nmhmcn  24189  ncvs1  24226  iscau4  24348  caussi  24366  cmssmscld  24419  cmslssbn  24441  cniccbdd  24530  ovoliunnul  24576  mbfinf  24734  itg2splitlem  24818  dvcn  24990  c1lip1  25066  c1lip3  25068  dvcnvrelem1  25086  ply1divex  25206  quotcan  25374  aannenlem1  25393  taylf  25425  ulmcaulem  25458  ulmcau  25459  reeff1o  25511  logccv  25723  logreclem  25817  isosctrlem2  25874  xrlimcnp  26023  rlimcxp  26028  ftalem7  26133  vmappw  26170  fsumvma  26266  dchreq  26311  dchrptlem1  26317  dchrsum  26322  bposlem7  26343  lgsqrlem2  26400  lgsdchr  26408  gausslemma2dlem1a  26418  lgseisenlem2  26429  lgsquad2  26439  2lgslem1b  26445  2sqlem6  26476  2sqnn0  26491  addsq2reu  26493  2sqreulem2  26505  tgcgrcomimp  26742  isperp2  26980  xmstrkgc  27156  brbtwn  27170  brcgr  27171  axcgrid  27187  axeuclidlem  27233  axeuclid  27234  elntg2  27256  lpvtx  27341  upgrex  27365  upgrpredgv  27412  upgredgpr  27415  uhgr0v0e  27508  subgrprop  27543  fusgrfisbase  27598  edgnbusgreu  27637  nbusgredgeu0  27638  cusgredg  27694  structtocusgr  27716  cusgrsize2inds  27723  cusgrsize  27724  usgredgsscusgredg  27729  fusgrmaxsize  27734  uspgrloopvtxel  27786  umgr2v2e  27795  vtxdginducedm1fi  27814  finsumvtxdg2sstep  27819  rgrprop  27830  rusgrprop  27832  0uhgrrusgr  27848  rusgrpropedg  27854  ewlkprop  27873  upgrewlkle2  27876  wlkprop  27881  upgrwlkcompim  27912  uspgr2wlkeq  27915  wlklenvclwlk  27924  wlklenvclwlkOLD  27925  wlkonprop  27928  wlkres  27940  redwlk  27942  wlkdlem2  27953  wksonproplem  27974  usgr2trlspth  28030  usgr2pth  28033  pthdlem1  28035  crctcshwlkn0lem4  28079  wwlksnprcl  28105  wlkiswwlks2  28141  wwlksm1edg  28147  wlknewwlksn  28153  wwlksnred  28158  wwlksnextbi  28160  wwlksnextwrd  28163  wwlksnextinj  28165  wwlksnextsurj  28166  umgr2wlk  28215  umgrwwlks2on  28223  elwwlks2  28232  clwwlk1loop  28253  umgrclwwlkge2  28256  clwlkclwwlklem2a1  28257  clwlkclwwlklem2a4  28262  clwlkclwwlklem2a  28263  clwlkclwwlklem2  28265  clwlkclwwlkfo  28274  clwwisshclwwslemlem  28278  clwwlknwwlksn  28303  clwwlknlbonbgr1  28304  clwwlkn1loopb  28308  clwwlkf  28312  clwwlknon1  28362  clwwlknonwwlknonb  28371  clwwlknonex2lem2  28373  vdn0conngrumgrv2  28461  frgrnbnb  28558  frgrncvvdeqlem2  28565  frgrncvvdeqlem3  28566  frgrncvvdeqlem6  28569  frgrwopreglem4a  28575  fusgr2wsp2nb  28599  frrusgrord0lem  28604  numclwwlk2lem1lem  28607  2clwwlk2clwwlklem  28611  2clwwlk2clwwlk  28615  numclwwlk1lem2foa  28619  numclwwlk1lem2f1  28622  frgrreg  28659  hlipgt0  29177  ocin  29559  ocnel  29561  shmodsi  29652  pjmf1  29979  unopf1o  30179  staddi  30509  stadd3i  30511  mdi  30558  dmdmd  30563  dmdi  30565  dmdbr2  30566  dmdbr3  30568  dmdbr4  30569  dmdi4  30570  mdsl1i  30584  superpos  30617  cvbr4i  30630  atssma  30641  atcv1  30643  atomli  30645  chirredlem1  30653  addltmulALT  30709  bian1d  30710  ifeqeqx  30786  disjxpin  30828  suppss3  30961  fpwrelmap  30970  prmdvdsbc  31032  ogrpaddlt  31245  metider  31746  tpr2rico  31764  xrge0iifiso  31787  qqhcn  31841  qqhucn  31842  esumlub  31928  esumpinfval  31941  esumpinfsum  31945  ballotlemfc0  32359  ballotlemfcc  32360  ftc2re  32478  bnj517  32765  fnrelpredd  32961  hashfundm  32974  pfxwlk  32985  subgrwlk  32994  loop1cycl  32999  erdsze2lem2  33066  satfv1  33225  satfdmlem  33230  satf0op  33239  fmlasuc  33248  poseq  33729  soseq  33730  sltval2  33786  sltres  33792  nodenselem8  33821  nodense  33822  noresle  33827  scutun12  33931  madeval2  33964  elmade  33978  dfrdg4  34180  altopthsn  34190  btwncomim  34242  btwnexch3  34249  btwnexch2  34252  endofsegid  34314  opnrebl2  34437  nn0prpwlem  34438  onsuct0  34557  ordcmp  34563  nndivsub  34573  dnibndlem13  34597  bj-cbval  34757  bj-cbvex  34758  bj-cbvexw  34784  bj-cbv3tb  34896  bj-spimtv  34903  bj-equsal  34936  bj-sbsb  34947  bj-vtoclf  35027  bj-zfauscl  35039  bj-gabss  35050  bj-gabeqd  35052  currysetlem2  35064  bj-snsetex  35080  bj-ismooredr2  35208  bj-inftyexpiinj  35307  bj-finsumval0  35383  bj-fvimacnv0  35384  bj-bary1lem1  35409  bj-bary1  35410  f1omptsnlem  35434  iooelexlt  35460  relowlpssretop  35462  rdgeqoa  35468  finxpsuclem  35495  fvineqsneq  35510  pibt2  35515  wl-equsal1i  35629  wl-ax11-lem10  35672  ltflcei  35692  sin2h  35694  cos2h  35695  tan2h  35696  lindsenlbs  35699  matunitlindf  35702  poimirlem3  35707  poimirlem4  35708  poimirlem18  35722  poimirlem20  35724  poimirlem21  35725  poimirlem22  35726  poimirlem24  35728  poimirlem25  35729  poimirlem26  35730  poimirlem27  35731  poimirlem28  35732  poimirlem31  35735  poimir  35737  heicant  35739  mblfinlem1  35741  mblfinlem2  35742  mblfinlem3  35743  mblfinlem4  35744  mbfresfi  35750  cnambfre  35752  ftc1anc  35785  dvasin  35788  areacirclem1  35792  areacirclem4  35795  areacirc  35797  brabg2  35801  fzmul  35826  fdc  35830  incsequz2  35834  isbnd2  35868  opidonOLD  35937  opidon2OLD  35939  grpomndo  35960  elghomlem2OLD  35971  rngoueqz  36025  dvrunz  36039  divrngidl  36113  dral1-o  36845  lsatn0  36940  l1cvpat  36995  leat2  37235  atnle  37258  cvlcvr1  37280  cvrexchlem  37360  cvratlem  37362  cvrat  37363  atcvrj0  37369  atle  37377  snatpsubN  37691  linepsubN  37693  pmapsub  37709  lneq2at  37719  lncvrelatN  37722  2llnma3r  37729  cdlemblem  37734  paddasslem5  37765  poml4N  37894  lhpmcvr4N  37967  trlval2  38104  cdlemd6  38144  cdleme7ga  38189  cdleme25b  38295  cdleme29b  38316  cdleme35fnpq  38390  cdleme50f1  38484  cdlemf1  38502  cdlemg27b  38637  cdlemk28-3  38849  tendospcanN  38964  diaf11N  38990  dia2dimlem1  39005  dibf11N  39102  dihf11  39208  dihmeetlem1N  39231  dochvalr  39298  dochnel2  39333  dvh4dimlem  39384  dochsat0  39398  mapd1o  39589  hdmapf1oN  39806  hgmapval0  39833  hgmapf1oN  39844  hlhilhillem  39905  nnproddivdvdsd  39937  lcmineqlem  39988  aks4d1p1p5  40011  aks4d1p3  40014  aks4d1p8d2  40021  aks4d1p8  40023  aks4d1p9  40024  sticksstones1  40030  sticksstones3  40032  sticksstones8  40037  sticksstones11  40040  sticksstones12  40042  sticksstones20  40050  sticksstones22  40052  metakunt7  40059  sn-axprlem3  40114  frlmsnic  40188  fsuppind  40202  oexpreposd  40242  rtprmirr  40268  prjspval  40363  rexrabdioph  40532  fphpdo  40555  irrapxlem3  40562  rmxypairf1o  40649  rmxycomplete  40655  zindbi  40684  lermxnn0  40688  ltrmy  40690  rmyeq0  40691  rmyeq  40692  lermy  40693  acongsym  40714  acongneg2  40715  wepwsolem  40783  intabssd  41024  iscard4  41038  ss2iundf  41156  frege129d  41260  frege133d  41262  axfrege52a  41353  axfrege52c  41384  ntrk0kbimka  41538  gneispace  41633  suprleubrd  41666  suprlubrd  41668  radcnvrat  41821  nzss  41824  expgrowthi  41840  ordpss  41958  bi23impib  41994  bi23imp13  42000  rspsbc2  42043  tratrb  42045  sbcim2g  42047  truniALT  42050  3impcombi  42326  tpid3gVD  42351  orbi1rVD  42357  sbc3orgVD  42360  rspsbc2VD  42364  tratrbVD  42370  sbcim2gVD  42384  sbcbiVD  42385  truniALTVD  42387  trintALTVD  42389  trintALT  42390  csbingVD  42393  csbsngVD  42402  csbxpgVD  42403  csbresgVD  42404  csbrngVD  42405  csbima12gALTVD  42406  csbunigVD  42407  csbfv12gALTVD  42408  relopabVD  42410  isosctrlem1ALT  42443  fzisoeu  42729  xrralrecnnge  42820  allbutfi  42823  climinf  43037  liminfreuzlem  43233  climliminf  43237  climliminflimsup  43239  xlimpnfxnegmnf  43245  xlimbr  43258  stoweidlem7  43438  stoweidlem62  43493  sge0gerpmpt  43830  meaiuninclem  43908  carageniuncllem2  43950  issmflem  44150  funressnfv  44424  funressnvmo  44426  f1cof1b  44456  2reu3  44489  ralbinrald  44501  afv0fv0  44528  afv0nbfvbi  44530  afvfv0bi  44531  fnbrafvb  44533  afvres  44551  tz6.12-afv  44552  afvco2  44555  ndmaovcl  44582  afv2res  44618  tz6.12-afv2  44619  nelbrim  44654  f1oresf1o2  44670  zm1nn  44682  nltle2tri  44693  subsubelfzo0  44706  iccpartres  44758  iccpartiltu  44762  fargshiftfv  44779  ichnreuop  44812  ichreuopeq  44813  prsprel  44827  sprsymrelf1lem  44831  sprsymrelfolem2  44833  sprsymrelfo  44837  prpair  44841  paireqne  44851  sbcpr  44861  fmtnof1  44875  goldbachthlem2  44886  fmtnoprmfac1  44905  fmtnoprmfac2  44907  lighneallem2  44946  lighneallem4b  44949  lighneallem4  44950  evennodd  44983  oddneven  44984  oexpnegnz  45018  evenltle  45057  fpprwppr  45079  fpprwpprb  45080  gbowge7  45103  gbege6  45105  sbgoldbwt  45117  sbgoldbst  45118  nnsum3primesle9  45134  bgoldbtbndlem2  45146  isomuspgrlem1  45167  isomuspgrlem2b  45169  isomuspgrlem2c  45170  isomuspgrlem2d  45171  mgmpropd  45217  clintop  45290  isassintop  45292  lidldomn1  45367  uzlidlring  45375  2zrngnmlid2  45397  rngccatidALTV  45435  ringccatidALTV  45498  srhmsubc  45522  srhmsubcALTV  45540  ztprmneprm  45571  pgrpgt2nabl  45590  lindslinindimp2lem4  45690  lincresunit3  45710  fldivexpfllog2  45799  digexp  45841  naryfvalelfv  45866  affinecomb1  45936  eenglngeehlnmlem1  45971  eenglngeehlnmlem2  45972  eenglngeehlnm  45973  itscnhlc0yqe  45993  itsclc0yqsol  45998  itscnhlc0xyqsol  45999  itschlc0xyqsol1  46000  itschlc0xyqsol  46001  itsclquadeu  46011  inlinecirc02plem  46020  inlinecirc02p  46021  pm4.71da  46023  mofsn  46059  seposep  46107  idmon  46185  idepi  46186  prsthinc  46223  grptcmon  46263  grptcepi  46264  spd  46270  spcdvw  46271  setrec2fun  46284