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  477  alexbii  1834  spvv  1999  spfw  2035  cbvalw  2037  sbequi  2086  chvarfv  2232  cbvalv1  2337  spv  2392  chvar  2394  cbval  2397  sb1  2478  nfsb4t  2502  exmoeu  2580  euim  2618  2eu3  2654  eqrdav  2736  ralbida  3250  raleleq  3314  rgen2a  3341  ralcom2  3347  ceqsalgALT  3474  vtoclf  3506  spcdv  3542  rspcdv  3562  rspcebdv  3564  rexraleqim  3586  elabgtOLD  3614  sbcn1  3781  sbcim1OLD  3783  sbcbi1  3787  sbeqalb  3794  sbcel21v  3799  disj  4392  elpwunsn  4629  rabsnifsb  4668  ssunsn2  4772  preqr1g  4795  iuneqconst  4948  axprlem3  5363  sbcop1  5421  propeqop  5440  euotd  5446  rexopabb  5461  sotr2  5553  relop  5780  elinxp  5949  elimasni  6017  sotri2  6057  onmindif  6380  iotavalOLD  6440  dffv2  6903  mpteqb  6934  elfvmptrab  6943  chfnrn  6966  elpreima  6975  iinpreima  6986  exfo  7021  ffnfv  7032  f1elima  7176  f1eqcocnv  7213  f1eqcocnvOLD  7214  fliftfun  7223  soisores  7238  isotr  7247  isomin  7248  ovmpodv2  7473  difsnexi  7653  onint  7682  oneqmin  7692  ordunisuc2  7737  tfindsg  7754  findsg  7793  f1oweALT  7862  el2mpocl  7973  poseq  8024  soseq  8025  ressuppss  8048  funsssuppss  8055  suppofssd  8068  smoiso  8242  seqomlem2  8331  oaordi  8427  oawordri  8431  oaordex  8439  oalimcl  8441  omwordi  8452  oewordi  8472  oelim2  8476  nnmwordi  8516  xpider  8627  iiner  8628  undifixp  8772  mptelixpg  8773  dom2lem  8832  findcard2s  9009  pssnn  9012  nneneq  9053  nneneqOLD  9065  fineqvlem  9106  pssnnOLD  9109  dif1ennnALT  9121  unfilem2  9155  xpfiOLD  9162  domunfican  9164  f1dmvrnfibi  9180  fsuppimp  9211  dffi2  9259  infsupprpr  9340  wemaplem2  9383  suc11reg  9455  noinfep  9496  cantnflem1  9525  r1fin  9609  tcrank  9720  cardlim  9808  pr2nelemOLD  9839  fseqenlem1  9860  alephnbtwn  9907  alephord2i  9913  alephf1  9921  cardaleph  9925  alephiso  9934  dfac12lem2  9980  ackbij1lem16  10071  cflm  10086  cfcoflem  10108  sornom  10113  fin23lem27  10164  isf32lem7  10195  fin17  10230  fin1a2lem2  10237  fin1a2lem4  10239  fin1a2lem6  10241  fin1a2lem9  10244  axdc3lem2  10287  zorn2lem7  10338  uniimadom  10380  inar1  10611  grothomex  10665  addcanpi  10735  mulcanpi  10736  enqer  10757  genpcd  10842  genpnmax  10843  ltexprlem4  10875  reclem3pr  10885  reclem4pr  10886  suplem2pr  10889  axpre-ltadd  11003  axpre-sup  11005  ltletr  11147  00id  11230  addn0nid  11475  mul0or  11695  prodgt02  11903  lemul1a  11909  mulgt1  11914  divgt0  11923  divge0  11924  ledivp1i  11980  ltdivp1i  11981  cju  12049  nnsub  12097  nominpos  12290  nn0n0n1ge2  12380  btwnnz  12476  suprfinzcl  12516  ublbneg  12753  zmax  12765  cnref1o  12805  ltsubrp  12846  ltaddrp  12847  xrltletr  12971  qbtwnre  13013  xltnegi  13030  xnn0xadd0  13061  iccsupr  13254  icoshft  13285  difreicc  13296  iccshftri  13299  iccshftli  13301  iccdili  13303  icccntri  13305  fzen  13353  elfz1b  13405  fzofzim  13514  eluzgtdifelfzo  13529  elfzo1elm1fzo0  13568  injresinjlem  13587  injresinj  13588  flval2  13614  flval3  13615  modmuladdim  13714  modaddmodup  13734  addmodlteq  13746  fseqsupubi  13778  ssnn0fi  13785  mptnn0fsuppr  13799  sq01  14020  hashf1rn  14146  hashgt12el  14216  hashgt12el2  14217  hash2pr  14262  hash2exprb  14264  hashge2el2difr  14274  hashtpg  14278  hash3tr  14283  lswlgt0cl  14351  ccatalpha  14377  pfxfv  14474  pfxsuff1eqwrdeq  14491  ccatopth2  14509  swrdccat  14527  swrdccat3blem  14531  reuccatpfxs1lem  14538  repsdf2  14570  repswsymball  14571  repswrevw  14579  cshweqrep  14613  cshw1  14614  2cshwcshw  14617  scshwfzeqfzo  14618  cshwcsh2id  14620  swrdco  14629  swrd2lsw  14744  2swrd2eqwrdeq  14745  wwlktovfo  14752  cjre  14929  icodiamlt  15226  reusq0  15253  o1lo1  15325  o1of2  15401  o1rlimmul  15407  zsum  15509  modfsummods  15584  zprod  15726  reeff1  15908  dvdsmod0  16048  dvds2lem  16057  muldvds1  16069  dvdscmulr  16073  dvdsmulcr  16074  dvdsdivcl  16104  mod2eq1n2dvds  16135  oddnn02np1  16136  divalglem8  16188  ndvdsadd  16198  zeqzmulgcd  16296  dfgcd2  16333  absproddvds  16399  lcmftp  16418  coprmdvds  16435  2mulprm  16475  isprm5  16489  divgcdodd  16492  isprm6  16496  prmdvdsexpr  16499  cncongrprm  16510  phiprmpw  16554  modprm0  16583  pythagtriplem4  16597  pcz  16659  difsqpwdvds  16665  1arith  16705  prmgaplem5  16833  prmgaplem6  16834  cshwrepswhash1  16881  divsfval  17335  catsubcat  17631  fthmon  17720  isinitoi  17791  istermoi  17792  iszeroi  17801  setcmon  17879  setcepi  17880  funcestrcsetclem8  17941  fthestrcsetc  17944  funcsetcestrclem8  17956  fthsetcestrc  17959  odupos  18123  pltnle  18133  pltval3  18134  lublecllem  18155  latasym  18238  mrelatglb  18355  mrelatlub  18357  cnvpsb  18374  isgrpid2  18692  ghmghmrn  18929  ghmf1  18939  orbsta  18995  resscntz  19014  gsmsymgrfixlem1  19111  gsmsymgreqlem2  19115  mndodcongi  19227  odf1  19245  lsmss1  19346  lsmss2  19348  efgredeu  19433  cntzcmnss  19517  lt6abl  19571  ablfaclem3  19765  ringinvnz1ne0  19906  kerf1ghm  20062  lspsneq  20467  lspsneu  20468  lsmcv  20486  lidldvgen  20609  0ringnnzr  20623  domnmuln0  20652  opprdomn  20655  domnchr  20819  znf1o  20842  zntoslem  20847  znfld  20851  cygznlem2a  20858  cygznlem3  20860  phlssphl  20947  islindf4  21128  uvcendim  21137  ply1scln0  21545  gsummoncoe1  21558  matvscl  21663  scmataddcl  21748  scmatsubcl  21749  scmatfo  21762  scmatghm  21765  maducoeval2  21872  slesolinv  21912  cramerimplem2  21916  cpmatelimp  21944  cpmatelimp2  21946  cpmatacl  21948  cpmatinvcl  21949  pm2mpf1  22031  cayhamlem1  22098  cayleyhamilton1  22124  0ntr  22305  islpi  22383  lmss  22532  cmpcld  22636  cmpfi  22642  1stcelcls  22695  comppfsc  22766  ptcnplem  22855  qtophmeo  23051  fbdmn0  23068  fbasrn  23118  elfm3  23184  fmfnfmlem4  23191  fclscf  23259  cnpfcf  23275  alexsubALTlem3  23283  tsmsres  23378  blval2  23801  tnggrpr  23902  nmoleub  23978  nmhmcn  24366  ncvs1  24404  iscau4  24526  caussi  24544  cmssmscld  24597  cmslssbn  24619  cniccbdd  24708  ovoliunnul  24754  mbfinf  24912  itg2splitlem  24996  dvcn  25168  c1lip1  25244  c1lip3  25246  dvcnvrelem1  25264  ply1divex  25384  quotcan  25552  aannenlem1  25571  taylf  25603  ulmcaulem  25636  ulmcau  25637  reeff1o  25689  logccv  25901  logreclem  25995  isosctrlem2  26052  xrlimcnp  26201  rlimcxp  26206  ftalem7  26311  vmappw  26348  fsumvma  26444  dchreq  26489  dchrptlem1  26495  dchrsum  26500  bposlem7  26521  lgsqrlem2  26578  lgsdchr  26586  gausslemma2dlem1a  26596  lgseisenlem2  26607  lgsquad2  26617  2lgslem1b  26623  2sqlem6  26654  2sqnn0  26669  addsq2reu  26671  2sqreulem2  26683  sltval2  26887  sltres  26893  nodenselem8  26922  nodense  26923  tgcgrcomimp  26974  isperp2  27212  xmstrkgc  27389  brbtwn  27403  brcgr  27404  axcgrid  27420  axeuclidlem  27466  axeuclid  27467  elntg2  27489  lpvtx  27574  upgrex  27598  upgrpredgv  27645  upgredgpr  27648  uhgr0v0e  27741  subgrprop  27776  fusgrfisbase  27831  edgnbusgreu  27870  nbusgredgeu0  27871  cusgredg  27927  structtocusgr  27949  cusgrsize2inds  27956  cusgrsize  27957  usgredgsscusgredg  27962  fusgrmaxsize  27967  uspgrloopvtxel  28019  umgr2v2e  28028  vtxdginducedm1fi  28047  finsumvtxdg2sstep  28052  rgrprop  28063  rusgrprop  28065  0uhgrrusgr  28081  rusgrpropedg  28087  ewlkprop  28106  upgrewlkle2  28109  wlkprop  28114  upgrwlkcompim  28146  uspgr2wlkeq  28149  wlklenvclwlk  28158  wlklenvclwlkOLD  28159  wlkonprop  28162  wlkres  28174  redwlk  28176  wlkdlem2  28187  wksonproplem  28208  wksonproplemOLD  28209  usgr2trlspth  28265  usgr2pth  28268  pthdlem1  28270  crctcshwlkn0lem4  28314  wwlksnprcl  28340  wlkiswwlks2  28376  wwlksm1edg  28382  wlknewwlksn  28388  wwlksnred  28393  wwlksnextbi  28395  wwlksnextwrd  28398  wwlksnextinj  28400  wwlksnextsurj  28401  umgr2wlk  28450  umgrwwlks2on  28458  elwwlks2  28467  clwwlk1loop  28488  umgrclwwlkge2  28491  clwlkclwwlklem2a1  28492  clwlkclwwlklem2a4  28497  clwlkclwwlklem2a  28498  clwlkclwwlklem2  28500  clwlkclwwlkfo  28509  clwwisshclwwslemlem  28513  clwwlknwwlksn  28538  clwwlknlbonbgr1  28539  clwwlkn1loopb  28543  clwwlkf  28547  clwwlknon1  28597  clwwlknonwwlknonb  28606  clwwlknonex2lem2  28608  vdn0conngrumgrv2  28696  frgrnbnb  28793  frgrncvvdeqlem2  28800  frgrncvvdeqlem3  28801  frgrncvvdeqlem6  28804  frgrwopreglem4a  28810  fusgr2wsp2nb  28834  frrusgrord0lem  28839  numclwwlk2lem1lem  28842  2clwwlk2clwwlklem  28846  2clwwlk2clwwlk  28850  numclwwlk1lem2foa  28854  numclwwlk1lem2f1  28857  frgrreg  28894  hlipgt0  29412  ocin  29794  ocnel  29796  shmodsi  29887  pjmf1  30214  unopf1o  30414  staddi  30744  stadd3i  30746  mdi  30793  dmdmd  30798  dmdi  30800  dmdbr2  30801  dmdbr3  30803  dmdbr4  30804  dmdi4  30805  mdsl1i  30819  superpos  30852  cvbr4i  30865  atssma  30876  atcv1  30878  atomli  30880  chirredlem1  30888  addltmulALT  30944  bian1d  30945  ifeqeqx  31020  disjxpin  31062  suppss3  31194  fpwrelmap  31203  prmdvdsbc  31265  ogrpaddlt  31478  metider  31984  tpr2rico  32002  xrge0iifiso  32025  qqhcn  32081  qqhucn  32082  esumlub  32168  esumpinfval  32181  esumpinfsum  32185  ballotlemfc0  32599  ballotlemfcc  32600  ftc2re  32718  bnj517  33004  fnrelpredd  33200  hashfundm  33213  pfxwlk  33224  subgrwlk  33233  loop1cycl  33238  erdsze2lem2  33305  satfv1  33464  satfdmlem  33469  satf0op  33478  fmlasuc  33487  noresle  33974  scutun12  34078  madeval2  34111  elmade  34125  dfrdg4  34327  altopthsn  34337  btwncomim  34389  btwnexch3  34396  btwnexch2  34399  endofsegid  34461  opnrebl2  34584  nn0prpwlem  34585  onsuct0  34704  ordcmp  34710  nndivsub  34720  dnibndlem13  34744  bj-cbval  34904  bj-cbvex  34905  bj-cbvexw  34931  bj-cbv3tb  35043  bj-spimtv  35050  bj-equsal  35082  bj-sbsb  35093  bj-vtoclf  35173  bj-zfauscl  35185  bj-gabss  35196  bj-gabeqd  35198  currysetlem2  35210  bj-snsetex  35225  bj-ismooredr2  35353  bj-inftyexpiinj  35452  bj-finsumval0  35528  bj-fvimacnv0  35529  bj-bary1lem1  35554  bj-bary1  35555  f1omptsnlem  35579  iooelexlt  35605  relowlpssretop  35607  rdgeqoa  35613  finxpsuclem  35640  fvineqsneq  35655  pibt2  35660  wl-equsal1i  35774  wl-ax11-lem10  35817  ltflcei  35837  sin2h  35839  cos2h  35840  tan2h  35841  lindsenlbs  35844  matunitlindf  35847  poimirlem3  35852  poimirlem4  35853  poimirlem18  35867  poimirlem20  35869  poimirlem21  35870  poimirlem22  35871  poimirlem24  35873  poimirlem25  35874  poimirlem26  35875  poimirlem27  35876  poimirlem28  35877  poimirlem31  35880  poimir  35882  heicant  35884  mblfinlem1  35886  mblfinlem2  35887  mblfinlem3  35888  mblfinlem4  35889  mbfresfi  35895  cnambfre  35897  ftc1anc  35930  dvasin  35933  areacirclem1  35937  areacirclem4  35940  areacirc  35942  brabg2  35946  fzmul  35971  fdc  35975  incsequz2  35979  isbnd2  36013  opidonOLD  36082  opidon2OLD  36084  grpomndo  36105  elghomlem2OLD  36116  rngoueqz  36170  dvrunz  36184  divrngidl  36258  refressn  36677  dral1-o  37138  lsatn0  37233  l1cvpat  37288  leat2  37528  atnle  37551  cvlcvr1  37573  cvrexchlem  37654  cvratlem  37656  cvrat  37657  atcvrj0  37663  atle  37671  snatpsubN  37985  linepsubN  37987  pmapsub  38003  lneq2at  38013  lncvrelatN  38016  2llnma3r  38023  cdlemblem  38028  paddasslem5  38059  poml4N  38188  lhpmcvr4N  38261  trlval2  38398  cdlemd6  38438  cdleme7ga  38483  cdleme25b  38589  cdleme29b  38610  cdleme35fnpq  38684  cdleme50f1  38778  cdlemf1  38796  cdlemg27b  38931  cdlemk28-3  39143  tendospcanN  39258  diaf11N  39284  dia2dimlem1  39299  dibf11N  39396  dihf11  39502  dihmeetlem1N  39525  dochvalr  39592  dochnel2  39627  dvh4dimlem  39678  dochsat0  39692  mapd1o  39883  hdmapf1oN  40100  hgmapval0  40127  hgmapf1oN  40138  hlhilhillem  40199  nnproddivdvdsd  40230  lcmineqlem  40281  aks4d1p1p5  40304  aks4d1p3  40307  aks4d1p8d2  40314  aks4d1p8  40316  aks4d1p9  40317  fldhmf1  40319  aks6d1c2p2  40321  sticksstones1  40326  sticksstones3  40328  sticksstones8  40333  sticksstones11  40336  sticksstones12  40338  sticksstones20  40346  sticksstones22  40348  metakunt7  40355  sn-axprlem3  40410  frlmsnic  40479  fsuppind  40495  oexpreposd  40537  rtprmirr  40563  prjspval  40658  rexrabdioph  40832  fphpdo  40855  irrapxlem3  40862  rmxypairf1o  40950  rmxycomplete  40956  zindbi  40985  lermxnn0  40989  ltrmy  40991  rmyeq0  40992  rmyeq  40993  lermy  40994  acongsym  41015  acongneg2  41016  wepwsolem  41084  naddcnffo  41276  intabssd  41360  iscard4  41374  ss2iundf  41501  frege129d  41605  frege133d  41607  axfrege52a  41698  axfrege52c  41729  ntrk0kbimka  41883  gneispace  41978  suprleubrd  42011  suprlubrd  42013  radcnvrat  42166  nzss  42169  expgrowthi  42185  ordpss  42303  bi23impib  42339  bi23imp13  42345  rspsbc2  42388  tratrb  42390  sbcim2g  42392  truniALT  42395  3impcombi  42671  tpid3gVD  42696  orbi1rVD  42702  sbc3orgVD  42705  rspsbc2VD  42709  tratrbVD  42715  sbcim2gVD  42729  sbcbiVD  42730  truniALTVD  42732  trintALTVD  42734  trintALT  42735  csbingVD  42738  csbsngVD  42747  csbxpgVD  42748  csbresgVD  42749  csbrngVD  42750  csbima12gALTVD  42751  csbunigVD  42752  csbfv12gALTVD  42753  relopabVD  42755  isosctrlem1ALT  42788  fzisoeu  43088  xrralrecnnge  43179  allbutfi  43182  climinf  43397  liminfreuzlem  43593  climliminf  43597  climliminflimsup  43599  xlimpnfxnegmnf  43605  xlimbr  43618  stoweidlem7  43798  stoweidlem62  43853  sge0gerpmpt  44191  meaiuninclem  44269  carageniuncllem2  44311  issmflem  44516  funressnfv  44802  funressnvmo  44804  f1cof1b  44834  2reu3  44867  ralbinrald  44879  afv0fv0  44906  afv0nbfvbi  44908  afvfv0bi  44909  fnbrafvb  44911  afvres  44929  tz6.12-afv  44930  afvco2  44933  ndmaovcl  44960  afv2res  44996  tz6.12-afv2  44997  nelbrim  45032  f1oresf1o2  45048  zm1nn  45059  nltle2tri  45070  subsubelfzo0  45083  iccpartres  45135  iccpartiltu  45139  fargshiftfv  45156  ichnreuop  45189  ichreuopeq  45190  prsprel  45204  sprsymrelf1lem  45208  sprsymrelfolem2  45210  sprsymrelfo  45214  prpair  45218  paireqne  45228  sbcpr  45238  fmtnof1  45252  goldbachthlem2  45263  fmtnoprmfac1  45282  fmtnoprmfac2  45284  lighneallem2  45323  lighneallem4b  45326  lighneallem4  45327  evennodd  45360  oddneven  45361  oexpnegnz  45395  evenltle  45434  fpprwppr  45456  fpprwpprb  45457  gbowge7  45480  gbege6  45482  sbgoldbwt  45494  sbgoldbst  45495  nnsum3primesle9  45511  bgoldbtbndlem2  45523  isomuspgrlem1  45544  isomuspgrlem2b  45546  isomuspgrlem2c  45547  isomuspgrlem2d  45548  mgmpropd  45594  clintop  45667  isassintop  45669  lidldomn1  45744  uzlidlring  45752  2zrngnmlid2  45774  rngccatidALTV  45812  ringccatidALTV  45875  srhmsubc  45899  srhmsubcALTV  45917  ztprmneprm  45948  pgrpgt2nabl  45967  lindslinindimp2lem4  46067  lincresunit3  46087  fldivexpfllog2  46176  digexp  46218  naryfvalelfv  46243  affinecomb1  46313  eenglngeehlnmlem1  46348  eenglngeehlnmlem2  46349  eenglngeehlnm  46350  itscnhlc0yqe  46370  itsclc0yqsol  46375  itscnhlc0xyqsol  46376  itschlc0xyqsol1  46377  itschlc0xyqsol  46378  itsclquadeu  46388  inlinecirc02plem  46397  inlinecirc02p  46398  pm4.71da  46400  mofsn  46436  seposep  46484  idmon  46562  idepi  46563  prsthinc  46600  grptcmon  46642  grptcepi  46643  spd  46649  spcdvw  46650  setrec2fun  46663  natlocalincr  46776  tworepnotupword  46786