Theorem biimpd 231

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  mpbid  234  sylibd  241  sylbid  242  mpbidi  243  syl5ib  246  syl6bi  255  con4bid  319  mtbird  327  mtbiri  329  imbi1d  344  bitr3  355  pm5.21im  377  biimpa  479  alexbii  1833  spvv  2003  spfw  2040  cbvalw  2042  alcomiwOLD  2051  sbbidvOLD  2085  sbequi  2091  chvarfv  2242  sbbidOLD  2248  cbvalv1  2361  spv  2411  chvar  2413  cbval  2416  sb1  2503  sb4OLD  2506  nfsb4t  2539  nfsb4tALT  2604  exmoeu  2666  euim  2701  2eu3  2738  eqrdav  2820  pm13.18  3097  rgen2a  3229  ralcom2  3363  raleleq  3427  ceqsalgALT  3530  vtoclf  3558  vtocl2OLD  3562  spcdv  3593  rspcdv  3615  rspcebdv  3617  rexraleqim  3640  elabgt  3663  sbcn1  3824  sbcim1  3825  sbcbi1  3830  sbeqalb  3836  sbcel21v  3842  elpwunsn  4621  rabsnifsb  4658  ssunsn2  4760  preqr1g  4783  iuneqconst  4930  axprlem3  5326  sbcop1  5379  propeqop  5397  euotd  5403  rexopabb  5415  sotr2  5505  relop  5721  elinxp  5890  elimasni  5956  sotri2  5989  onmindif  6280  iotaval  6329  dffv2  6756  mpteqb  6787  elfvmptrab  6796  chfnrn  6819  elpreima  6828  iinpreima  6837  exfo  6871  ffnfv  6882  f1elima  7021  f1eqcocnv  7057  fliftfun  7065  soisores  7080  isotr  7089  isomin  7090  ovmpodv2  7308  difsnexi  7483  onint  7510  oneqmin  7520  ordunisuc2  7559  tfindsg  7575  findsg  7609  f1oweALT  7673  el2mpocl  7781  ressuppss  7849  funsssuppss  7856  suppofssd  7867  imacosuppOLD  7875  smoiso  7999  seqomlem2  8087  oaordi  8172  oawordri  8176  oaordex  8184  oalimcl  8186  omwordi  8197  oewordi  8217  oelim2  8221  nnmwordi  8261  xpider  8368  iiner  8369  undifixp  8498  mptelixpg  8499  dom2lem  8549  nneneq  8700  fineqvlem  8732  pssnn  8736  dif1en  8751  findcard2s  8759  unfilem2  8783  xpfi  8789  domunfican  8791  f1dmvrnfibi  8808  fsuppimp  8839  dffi2  8887  infsupprpr  8968  wemaplem2  9011  suc11reg  9082  noinfep  9123  cantnflem1  9152  r1fin  9202  tcrank  9313  cardlim  9401  pr2nelem  9430  fseqenlem1  9450  alephnbtwn  9497  alephord2i  9503  alephf1  9511  cardaleph  9515  alephiso  9524  dfac12lem2  9570  ackbij1lem16  9657  cflm  9672  cfcoflem  9694  sornom  9699  fin23lem27  9750  isf32lem7  9781  fin17  9816  fin1a2lem2  9823  fin1a2lem4  9825  fin1a2lem6  9827  fin1a2lem9  9830  axdc3lem2  9873  zorn2lem7  9924  uniimadom  9966  inar1  10197  grothomex  10251  addcanpi  10321  mulcanpi  10322  enqer  10343  genpcd  10428  genpnmax  10429  ltexprlem4  10461  reclem3pr  10471  reclem4pr  10472  suplem2pr  10475  axpre-ltadd  10589  axpre-sup  10591  ltletr  10732  00id  10815  addn0nid  11060  mul0or  11280  prodgt02  11488  lemul1a  11494  mulgt1  11499  divgt0  11508  divge0  11509  ledivp1i  11565  ltdivp1i  11566  cju  11634  nnsub  11682  nominpos  11875  nn0n0n1ge2  11963  btwnnz  12059  suprfinzcl  12098  ublbneg  12334  zmax  12346  cnref1o  12385  ltsubrp  12426  ltaddrp  12427  xrltletr  12551  qbtwnre  12593  xltnegi  12610  xnn0xadd0  12641  iccsupr  12831  icoshft  12860  difreicc  12871  iccshftri  12874  iccshftli  12876  iccdili  12878  icccntri  12880  fzen  12925  elfz1b  12977  fzofzim  13085  eluzgtdifelfzo  13100  elfzo1elm1fzo0  13139  injresinjlem  13158  injresinj  13159  flval2  13185  flval3  13186  modmuladdim  13283  modaddmodup  13303  addmodlteq  13315  fseqsupubi  13347  ssnn0fi  13354  mptnn0fsuppr  13368  sq01  13587  hashf1rn  13714  hashgt12el  13784  hashgt12el2  13785  hash2pr  13828  hash2exprb  13830  hashge2el2difr  13840  hashtpg  13844  hash3tr  13849  lswlgt0cl  13921  ccatalpha  13947  pfxfv  14044  pfxsuff1eqwrdeq  14061  ccatopth2  14079  swrdccat  14097  swrdccat3blem  14101  reuccatpfxs1lem  14108  repsdf2  14140  repswsymball  14141  repswrevw  14149  cshweqrep  14183  cshw1  14184  2cshwcshw  14187  scshwfzeqfzo  14188  cshwcsh2id  14190  swrdco  14199  swrd2lsw  14314  2swrd2eqwrdeq  14315  wwlktovfo  14322  cjre  14498  icodiamlt  14795  reusq0  14822  o1lo1  14894  o1of2  14969  o1rlimmul  14975  zsum  15075  modfsummods  15148  zprod  15291  reeff1  15473  dvdsmod0  15613  dvds2lem  15622  muldvds1  15634  dvdscmulr  15638  dvdsmulcr  15639  dvdsdivcl  15666  mod2eq1n2dvds  15696  oddnn02np1  15697  divalglem8  15751  ndvdsadd  15761  zeqzmulgcd  15859  dfgcd2  15894  gcdmultipleOLD  15900  absproddvds  15961  lcmftp  15980  coprmdvds  15997  2mulprm  16037  isprm5  16051  divgcdodd  16054  isprm6  16058  prmdvdsexpr  16061  cncongrprm  16069  phiprmpw  16113  modprm0  16142  pythagtriplem4  16156  pcz  16217  difsqpwdvds  16223  1arith  16263  prmgaplem5  16391  prmgaplem6  16392  cshwrepswhash1  16436  divsfval  16820  catsubcat  17109  fthmon  17197  isinitoi  17263  istermoi  17264  iszeroi  17269  setcmon  17347  setcepi  17348  funcestrcsetclem8  17397  fthestrcsetc  17400  funcsetcestrclem8  17412  fthsetcestrc  17415  pltnle  17576  pltval3  17577  lublecllem  17598  latasym  17665  odupos  17745  mrelatglb  17794  mrelatlub  17796  cnvpsb  17823  isgrpid2  18140  ghmghmrn  18377  ghmf1  18387  orbsta  18443  resscntz  18462  gsmsymgrfixlem1  18555  gsmsymgreqlem2  18559  mndodcongi  18671  odf1  18689  lsmss1  18791  lsmss2  18793  efgredeu  18878  cntzcmnss  18961  lt6abl  19015  ablfaclem3  19209  ringinvnz1ne0  19342  kerf1ghm  19497  kerf1hrmOLD  19498  lspsneq  19894  lspsneu  19895  lsmcv  19913  lidldvgen  20028  0ringnnzr  20042  domnmuln0  20071  opprdomn  20074  ply1scln0  20459  gsummoncoe1  20472  domnchr  20679  znf1o  20698  zntoslem  20703  znfld  20707  cygznlem2a  20714  cygznlem3  20716  phlssphl  20803  islindf4  20982  uvcendim  20991  matvscl  21040  scmataddcl  21125  scmatsubcl  21126  scmatfo  21139  scmatghm  21142  maducoeval2  21249  slesolinv  21289  cramerimplem2  21293  cpmatelimp  21320  cpmatelimp2  21322  cpmatacl  21324  cpmatinvcl  21325  pm2mpf1  21407  cayhamlem1  21474  cayleyhamilton1  21500  0ntr  21679  islpi  21757  lmss  21906  cmpcld  22010  cmpfi  22016  1stcelcls  22069  comppfsc  22140  ptcnplem  22229  qtophmeo  22425  fbdmn0  22442  fbasrn  22492  elfm3  22558  fmfnfmlem4  22565  fclscf  22633  cnpfcf  22649  alexsubALTlem3  22657  tsmsres  22752  blval2  23172  tnggrpr  23264  nmoleub  23340  nmhmcn  23724  ncvs1  23761  iscau4  23882  caussi  23900  cmssmscld  23953  cmslssbn  23975  cniccbdd  24062  ovoliunnul  24108  mbfinf  24266  itg2splitlem  24349  dvcn  24518  c1lip1  24594  c1lip3  24596  dvcnvrelem1  24614  ply1divex  24730  quotcan  24898  aannenlem1  24917  taylf  24949  ulmcaulem  24982  ulmcau  24983  reeff1o  25035  logccv  25246  logreclem  25340  isosctrlem2  25397  xrlimcnp  25546  rlimcxp  25551  ftalem7  25656  vmappw  25693  fsumvma  25789  dchreq  25834  dchrptlem1  25840  dchrsum  25845  bposlem7  25866  lgsqrlem2  25923  lgsdchr  25931  gausslemma2dlem1a  25941  lgseisenlem2  25952  lgsquad2  25962  2lgslem1b  25968  2sqlem6  25999  2sqnn0  26014  addsq2reu  26016  2sqreulem2  26028  tgcgrcomimp  26263  isperp2  26501  xmstrkgc  26672  brbtwn  26685  brcgr  26686  axcgrid  26702  axeuclidlem  26748  axeuclid  26749  elntg2  26771  lpvtx  26853  upgrex  26877  upgrpredgv  26924  upgredgpr  26927  uhgr0v0e  27020  subgrprop  27055  fusgrfisbase  27110  edgnbusgreu  27149  nbusgredgeu0  27150  cusgredg  27206  structtocusgr  27228  cusgrsize2inds  27235  cusgrsize  27236  usgredgsscusgredg  27241  fusgrmaxsize  27246  uspgrloopvtxel  27298  umgr2v2e  27307  vtxdginducedm1fi  27326  finsumvtxdg2sstep  27331  rgrprop  27342  rusgrprop  27344  0uhgrrusgr  27360  rusgrpropedg  27366  ewlkprop  27385  upgrewlkle2  27388  wlkprop  27393  upgrwlkcompim  27424  uspgr2wlkeq  27427  wlklenvclwlk  27436  wlklenvclwlkOLD  27437  wlkonprop  27440  wlkres  27452  redwlk  27454  wlkdlem2  27465  wksonproplem  27486  usgr2trlspth  27542  usgr2pth  27545  pthdlem1  27547  crctcshwlkn0lem4  27591  wwlksnprcl  27617  wlkiswwlks2  27653  wwlksm1edg  27659  wlknewwlksn  27665  wwlksnred  27670  wwlksnextbi  27672  wwlksnextwrd  27675  wwlksnextinj  27677  wwlksnextsurj  27678  umgr2wlk  27728  umgrwwlks2on  27736  elwwlks2  27745  clwwlk1loop  27766  umgrclwwlkge2  27769  clwlkclwwlklem2a1  27770  clwlkclwwlklem2a4  27775  clwlkclwwlklem2a  27776  clwlkclwwlklem2  27778  clwlkclwwlkfo  27787  clwwisshclwwslemlem  27791  clwwlknwwlksn  27816  clwwlknlbonbgr1  27817  clwwlkn1loopb  27821  clwwlkf  27826  clwwlknon1  27876  clwwlknonwwlknonb  27885  clwwlknonex2lem2  27887  vdn0conngrumgrv2  27975  frgrnbnb  28072  frgrncvvdeqlem2  28079  frgrncvvdeqlem3  28080  frgrncvvdeqlem6  28083  frgrwopreglem4a  28089  fusgr2wsp2nb  28113  frrusgrord0lem  28118  numclwwlk2lem1lem  28121  2clwwlk2clwwlklem  28125  2clwwlk2clwwlk  28129  numclwwlk1lem2foa  28133  numclwwlk1lem2f1  28136  frgrreg  28173  hlipgt0  28691  ocin  29073  ocnel  29075  shmodsi  29166  pjmf1  29493  unopf1o  29693  staddi  30023  stadd3i  30025  mdi  30072  dmdmd  30077  dmdi  30079  dmdbr2  30080  dmdbr3  30082  dmdbr4  30083  dmdi4  30084  mdsl1i  30098  superpos  30131  cvbr4i  30144  atssma  30155  atcv1  30157  atomli  30159  chirredlem1  30167  addltmulALT  30223  bian1d  30224  ifeqeqx  30297  disjxpin  30338  suppss3  30460  fpwrelmap  30469  prmdvdsbc  30532  ogrpaddlt  30718  metider  31134  tpr2rico  31155  xrge0iifiso  31178  qqhcn  31232  qqhucn  31233  esumlub  31319  esumpinfval  31332  esumpinfsum  31336  ballotlemfc0  31750  ballotlemfcc  31751  ftc2re  31869  bnj517  32157  hashfundm  32354  pfxwlk  32370  subgrwlk  32379  loop1cycl  32384  erdsze2lem2  32451  satfv1  32610  satfdmlem  32615  satf0op  32624  fmlasuc  32633  trpredrec  33077  poseq  33095  soseq  33096  sltval2  33163  sltres  33169  nodenselem8  33195  nodense  33196  noresle  33200  scutun12  33271  madeval2  33290  dfrdg4  33412  altopthsn  33422  btwncomim  33474  btwnexch3  33481  btwnexch2  33484  endofsegid  33546  opnrebl2  33669  nn0prpwlem  33670  onsuct0  33789  ordcmp  33795  nndivsub  33805  dnibndlem13  33829  bj-cbval  33982  bj-cbvex  33983  bj-cbvexw  34009  bj-cbv3tb  34109  bj-spimtv  34116  bj-equsal  34149  bj-sbsb  34160  bj-vtoclf  34234  bj-zfauscl  34246  currysetlem2  34262  bj-snsetex  34278  bj-ismooredr2  34405  bj-inftyexpiinj  34494  bj-finsumval0  34570  bj-fvimacnv0  34571  bj-bary1lem1  34595  bj-bary1  34596  f1omptsnlem  34620  iooelexlt  34646  relowlpssretop  34648  rdgeqoa  34654  finxpsuclem  34681  fvineqsneq  34696  pibt2  34701  wl-equsal1i  34798  wl-ax11-lem10  34841  ltflcei  34895  sin2h  34897  cos2h  34898  tan2h  34899  lindsenlbs  34902  matunitlindf  34905  poimirlem3  34910  poimirlem4  34911  poimirlem18  34925  poimirlem20  34927  poimirlem21  34928  poimirlem22  34929  poimirlem24  34931  poimirlem25  34932  poimirlem26  34933  poimirlem27  34934  poimirlem28  34935  poimirlem31  34938  poimir  34940  heicant  34942  mblfinlem1  34944  mblfinlem2  34945  mblfinlem3  34946  mblfinlem4  34947  mbfresfi  34953  cnambfre  34955  ftc1anc  34990  dvasin  34993  areacirclem1  34997  areacirclem4  35000  areacirc  35002  brabg2  35006  fzmul  35031  fdc  35035  incsequz2  35039  isbnd2  35076  opidonOLD  35145  opidon2OLD  35147  grpomndo  35168  elghomlem2OLD  35179  rngoueqz  35233  dvrunz  35247  divrngidl  35321  dral1-o  36055  lsatn0  36150  l1cvpat  36205  leat2  36445  atnle  36468  cvlcvr1  36490  cvrexchlem  36570  cvratlem  36572  cvrat  36573  atcvrj0  36579  atle  36587  snatpsubN  36901  linepsubN  36903  pmapsub  36919  lneq2at  36929  lncvrelatN  36932  2llnma3r  36939  cdlemblem  36944  paddasslem5  36975  poml4N  37104  lhpmcvr4N  37177  trlval2  37314  cdlemd6  37354  cdleme7ga  37399  cdleme25b  37505  cdleme29b  37526  cdleme35fnpq  37600  cdleme50f1  37694  cdlemf1  37712  cdlemg27b  37847  cdlemk28-3  38059  tendospcanN  38174  diaf11N  38200  dia2dimlem1  38215  dibf11N  38312  dihf11  38418  dihmeetlem1N  38441  dochvalr  38508  dochnel2  38543  dvh4dimlem  38594  dochsat0  38608  mapd1o  38799  hdmapf1oN  39016  hgmapval0  39043  hgmapf1oN  39054  hlhilhillem  39111  sn-axprlem3  39158  frlmsnic  39198  oexpreposd  39228  rtprmirr  39243  prjspval  39302  rexrabdioph  39440  fphpdo  39463  irrapxlem3  39470  rmxypairf1o  39557  rmxycomplete  39563  zindbi  39592  lermxnn0  39596  ltrmy  39598  rmyeq0  39599  rmyeq  39600  lermy  39601  acongsym  39622  acongneg2  39623  wepwsolem  39691  intabssd  39934  iscard4  39949  ss2iundf  40053  frege129d  40157  frege133d  40159  axfrege52a  40251  axfrege52c  40282  ntrk0kbimka  40438  gneispace  40533  suprleubrd  40566  suprlubrd  40569  radcnvrat  40695  nzss  40698  expgrowthi  40714  ordpss  40832  bi23impib  40868  bi23imp13  40874  rspsbc2  40917  tratrb  40919  sbcim2g  40921  truniALT  40924  3impcombi  41200  tpid3gVD  41225  orbi1rVD  41231  sbc3orgVD  41234  rspsbc2VD  41238  tratrbVD  41244  sbcim2gVD  41258  sbcbiVD  41259  truniALTVD  41261  trintALTVD  41263  trintALT  41264  csbingVD  41267  csbsngVD  41276  csbxpgVD  41277  csbresgVD  41278  csbrngVD  41279  csbima12gALTVD  41280  csbunigVD  41281  csbfv12gALTVD  41282  relopabVD  41284  isosctrlem1ALT  41317  fzisoeu  41616  xrralrecnnge  41711  allbutfi  41714  climinf  41936  liminfreuzlem  42132  climliminf  42136  climliminflimsup  42138  xlimpnfxnegmnf  42144  xlimbr  42157  stoweidlem7  42341  stoweidlem62  42396  sge0gerpmpt  42733  meaiuninclem  42811  carageniuncllem2  42853  issmflem  43053  funressnfv  43327  funressnvmo  43329  2reu3  43358  ralbinrald  43370  afv0fv0  43397  afv0nbfvbi  43399  afvfv0bi  43400  fnbrafvb  43402  afvres  43420  tz6.12-afv  43421  afvco2  43424  ndmaovcl  43451  afv2res  43487  tz6.12-afv2  43488  nelbrim  43523  f1oresf1o2  43539  zm1nn  43551  nltle2tri  43562  subsubelfzo0  43575  iccpartres  43627  iccpartiltu  43631  fargshiftfv  43648  ichan  43679  ichnreuop  43683  ichreuopeq  43684  prsprel  43698  sprsymrelf1lem  43702  sprsymrelfolem2  43704  sprsymrelfo  43708  prpair  43712  paireqne  43722  sbcpr  43732  fmtnof1  43746  goldbachthlem2  43757  fmtnoprmfac1  43776  fmtnoprmfac2  43778  lighneallem2  43820  lighneallem4b  43823  lighneallem4  43824  evennodd  43857  oddneven  43858  oexpnegnz  43892  evenltle  43931  fpprwppr  43953  fpprwpprb  43954  gbowge7  43977  gbege6  43979  sbgoldbwt  43991  sbgoldbst  43992  nnsum3primesle9  44008  bgoldbtbndlem2  44020  isomuspgrlem1  44041  isomuspgrlem2b  44043  isomuspgrlem2c  44044  isomuspgrlem2d  44045  mgmpropd  44091  clintop  44164  isassintop  44166  lidldomn1  44241  uzlidlring  44249  2zrngnmlid2  44271  rngccatidALTV  44309  ringccatidALTV  44372  srhmsubc  44396  srhmsubcALTV  44414  ztprmneprm  44444  pgrpgt2nabl  44463  lindslinindimp2lem4  44565  lincresunit3  44585  fldivexpfllog2  44674  digexp  44716  affinecomb1  44738  eenglngeehlnmlem1  44773  eenglngeehlnmlem2  44774  eenglngeehlnm  44775  itscnhlc0yqe  44795  itsclc0yqsol  44800  itscnhlc0xyqsol  44801  itschlc0xyqsol1  44802  itschlc0xyqsol  44803  itsclquadeu  44813  inlinecirc02plem  44822  inlinecirc02p  44823  spd  44830  spcdvw  44831  setrec2fun  44844