Theorem biimpd 232

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  mpbid  235  sylibd  242  sylbid  243  mpbidi  244  syl5ib  247  syl6bi  256  con4bid  320  mtbird  328  mtbiri  330  imbi1d  345  bitr3  356  pm5.21im  378  biimpa  480  alexbii  1834  spvv  2003  spfw  2040  cbvalw  2042  alcomiwOLD  2051  sbequi  2089  chvarfv  2240  cbvalv1  2350  spv  2400  chvar  2402  cbval  2405  sb1  2492  sb4OLD  2495  nfsb4t  2517  nfsb4tALT  2580  exmoeu  2641  euim  2678  2eu3  2715  eqrdav  2797  pm13.18  3068  rgen2a  3193  ralcom2  3316  raleleq  3372  ceqsalgALT  3477  vtoclf  3506  vtocl2OLD  3510  spcdv  3541  rspcdv  3563  rspcebdv  3565  rexraleqim  3588  elabgt  3609  sbcn1  3771  sbcim1  3772  sbcbi1  3777  sbeqalb  3783  sbcel21v  3788  disj  4355  elpwunsn  4581  rabsnifsb  4618  ssunsn2  4720  preqr1g  4743  iuneqconst  4892  axprlem3  5291  sbcop1  5344  propeqop  5362  euotd  5368  rexopabb  5380  sotr2  5469  relop  5685  elinxp  5856  elimasni  5923  sotri2  5956  onmindif  6248  iotaval  6298  dffv2  6733  mpteqb  6764  elfvmptrab  6773  chfnrn  6796  elpreima  6805  iinpreima  6814  exfo  6848  ffnfv  6859  f1elima  6999  f1eqcocnv  7035  f1eqcocnvOLD  7036  fliftfun  7044  soisores  7059  isotr  7068  isomin  7069  ovmpodv2  7287  difsnexi  7463  onint  7490  oneqmin  7500  ordunisuc2  7539  tfindsg  7555  findsg  7590  f1oweALT  7655  el2mpocl  7764  ressuppss  7832  funsssuppss  7839  suppofssd  7850  imacosuppOLD  7858  smoiso  7982  seqomlem2  8070  oaordi  8155  oawordri  8159  oaordex  8167  oalimcl  8169  omwordi  8180  oewordi  8200  oelim2  8204  nnmwordi  8244  xpider  8351  iiner  8352  undifixp  8481  mptelixpg  8482  dom2lem  8532  nneneq  8684  fineqvlem  8716  pssnn  8720  dif1en  8735  findcard2s  8743  unfilem2  8767  xpfi  8773  domunfican  8775  f1dmvrnfibi  8792  fsuppimp  8823  dffi2  8871  infsupprpr  8952  wemaplem2  8995  suc11reg  9066  noinfep  9107  cantnflem1  9136  r1fin  9186  tcrank  9297  cardlim  9385  pr2nelem  9415  fseqenlem1  9435  alephnbtwn  9482  alephord2i  9488  alephf1  9496  cardaleph  9500  alephiso  9509  dfac12lem2  9555  ackbij1lem16  9646  cflm  9661  cfcoflem  9683  sornom  9688  fin23lem27  9739  isf32lem7  9770  fin17  9805  fin1a2lem2  9812  fin1a2lem4  9814  fin1a2lem6  9816  fin1a2lem9  9819  axdc3lem2  9862  zorn2lem7  9913  uniimadom  9955  inar1  10186  grothomex  10240  addcanpi  10310  mulcanpi  10311  enqer  10332  genpcd  10417  genpnmax  10418  ltexprlem4  10450  reclem3pr  10460  reclem4pr  10461  suplem2pr  10464  axpre-ltadd  10578  axpre-sup  10580  ltletr  10721  00id  10804  addn0nid  11049  mul0or  11269  prodgt02  11477  lemul1a  11483  mulgt1  11488  divgt0  11497  divge0  11498  ledivp1i  11554  ltdivp1i  11555  cju  11621  nnsub  11669  nominpos  11862  nn0n0n1ge2  11950  btwnnz  12046  suprfinzcl  12085  ublbneg  12321  zmax  12333  cnref1o  12372  ltsubrp  12413  ltaddrp  12414  xrltletr  12538  qbtwnre  12580  xltnegi  12597  xnn0xadd0  12628  iccsupr  12820  icoshft  12851  difreicc  12862  iccshftri  12865  iccshftli  12867  iccdili  12869  icccntri  12871  fzen  12919  elfz1b  12971  fzofzim  13079  eluzgtdifelfzo  13094  elfzo1elm1fzo0  13133  injresinjlem  13152  injresinj  13153  flval2  13179  flval3  13180  modmuladdim  13277  modaddmodup  13297  addmodlteq  13309  fseqsupubi  13341  ssnn0fi  13348  mptnn0fsuppr  13362  sq01  13582  hashf1rn  13709  hashgt12el  13779  hashgt12el2  13780  hash2pr  13823  hash2exprb  13825  hashge2el2difr  13835  hashtpg  13839  hash3tr  13844  lswlgt0cl  13912  ccatalpha  13938  pfxfv  14035  pfxsuff1eqwrdeq  14052  ccatopth2  14070  swrdccat  14088  swrdccat3blem  14092  reuccatpfxs1lem  14099  repsdf2  14131  repswsymball  14132  repswrevw  14140  cshweqrep  14174  cshw1  14175  2cshwcshw  14178  scshwfzeqfzo  14179  cshwcsh2id  14181  swrdco  14190  swrd2lsw  14305  2swrd2eqwrdeq  14306  wwlktovfo  14313  cjre  14490  icodiamlt  14787  reusq0  14814  o1lo1  14886  o1of2  14961  o1rlimmul  14967  zsum  15067  modfsummods  15140  zprod  15283  reeff1  15465  dvdsmod0  15605  dvds2lem  15614  muldvds1  15626  dvdscmulr  15630  dvdsmulcr  15631  dvdsdivcl  15658  mod2eq1n2dvds  15688  oddnn02np1  15689  divalglem8  15741  ndvdsadd  15751  zeqzmulgcd  15849  dfgcd2  15884  gcdmultipleOLD  15890  absproddvds  15951  lcmftp  15970  coprmdvds  15987  2mulprm  16027  isprm5  16041  divgcdodd  16044  isprm6  16048  prmdvdsexpr  16051  cncongrprm  16059  phiprmpw  16103  modprm0  16132  pythagtriplem4  16146  pcz  16207  difsqpwdvds  16213  1arith  16253  prmgaplem5  16381  prmgaplem6  16382  cshwrepswhash1  16428  divsfval  16812  catsubcat  17101  fthmon  17189  isinitoi  17255  istermoi  17256  iszeroi  17261  setcmon  17339  setcepi  17340  funcestrcsetclem8  17389  fthestrcsetc  17392  funcsetcestrclem8  17404  fthsetcestrc  17407  pltnle  17568  pltval3  17569  lublecllem  17590  latasym  17657  odupos  17737  mrelatglb  17786  mrelatlub  17788  cnvpsb  17815  isgrpid2  18132  ghmghmrn  18369  ghmf1  18379  orbsta  18435  resscntz  18454  gsmsymgrfixlem1  18547  gsmsymgreqlem2  18551  mndodcongi  18663  odf1  18681  lsmss1  18783  lsmss2  18785  efgredeu  18870  cntzcmnss  18954  lt6abl  19008  ablfaclem3  19202  ringinvnz1ne0  19338  kerf1ghm  19491  lspsneq  19887  lspsneu  19888  lsmcv  19906  lidldvgen  20021  0ringnnzr  20035  domnmuln0  20064  opprdomn  20067  domnchr  20224  znf1o  20243  zntoslem  20248  znfld  20252  cygznlem2a  20259  cygznlem3  20261  phlssphl  20348  islindf4  20527  uvcendim  20536  ply1scln0  20920  gsummoncoe1  20933  matvscl  21036  scmataddcl  21121  scmatsubcl  21122  scmatfo  21135  scmatghm  21138  maducoeval2  21245  slesolinv  21285  cramerimplem2  21289  cpmatelimp  21317  cpmatelimp2  21319  cpmatacl  21321  cpmatinvcl  21322  pm2mpf1  21404  cayhamlem1  21471  cayleyhamilton1  21497  0ntr  21676  islpi  21754  lmss  21903  cmpcld  22007  cmpfi  22013  1stcelcls  22066  comppfsc  22137  ptcnplem  22226  qtophmeo  22422  fbdmn0  22439  fbasrn  22489  elfm3  22555  fmfnfmlem4  22562  fclscf  22630  cnpfcf  22646  alexsubALTlem3  22654  tsmsres  22749  blval2  23169  tnggrpr  23261  nmoleub  23337  nmhmcn  23725  ncvs1  23762  iscau4  23883  caussi  23901  cmssmscld  23954  cmslssbn  23976  cniccbdd  24065  ovoliunnul  24111  mbfinf  24269  itg2splitlem  24352  dvcn  24524  c1lip1  24600  c1lip3  24602  dvcnvrelem1  24620  ply1divex  24737  quotcan  24905  aannenlem1  24924  taylf  24956  ulmcaulem  24989  ulmcau  24990  reeff1o  25042  logccv  25254  logreclem  25348  isosctrlem2  25405  xrlimcnp  25554  rlimcxp  25559  ftalem7  25664  vmappw  25701  fsumvma  25797  dchreq  25842  dchrptlem1  25848  dchrsum  25853  bposlem7  25874  lgsqrlem2  25931  lgsdchr  25939  gausslemma2dlem1a  25949  lgseisenlem2  25960  lgsquad2  25970  2lgslem1b  25976  2sqlem6  26007  2sqnn0  26022  addsq2reu  26024  2sqreulem2  26036  tgcgrcomimp  26271  isperp2  26509  xmstrkgc  26680  brbtwn  26693  brcgr  26694  axcgrid  26710  axeuclidlem  26756  axeuclid  26757  elntg2  26779  lpvtx  26861  upgrex  26885  upgrpredgv  26932  upgredgpr  26935  uhgr0v0e  27028  subgrprop  27063  fusgrfisbase  27118  edgnbusgreu  27157  nbusgredgeu0  27158  cusgredg  27214  structtocusgr  27236  cusgrsize2inds  27243  cusgrsize  27244  usgredgsscusgredg  27249  fusgrmaxsize  27254  uspgrloopvtxel  27306  umgr2v2e  27315  vtxdginducedm1fi  27334  finsumvtxdg2sstep  27339  rgrprop  27350  rusgrprop  27352  0uhgrrusgr  27368  rusgrpropedg  27374  ewlkprop  27393  upgrewlkle2  27396  wlkprop  27401  upgrwlkcompim  27432  uspgr2wlkeq  27435  wlklenvclwlk  27444  wlklenvclwlkOLD  27445  wlkonprop  27448  wlkres  27460  redwlk  27462  wlkdlem2  27473  wksonproplem  27494  usgr2trlspth  27550  usgr2pth  27553  pthdlem1  27555  crctcshwlkn0lem4  27599  wwlksnprcl  27625  wlkiswwlks2  27661  wwlksm1edg  27667  wlknewwlksn  27673  wwlksnred  27678  wwlksnextbi  27680  wwlksnextwrd  27683  wwlksnextinj  27685  wwlksnextsurj  27686  umgr2wlk  27735  umgrwwlks2on  27743  elwwlks2  27752  clwwlk1loop  27773  umgrclwwlkge2  27776  clwlkclwwlklem2a1  27777  clwlkclwwlklem2a4  27782  clwlkclwwlklem2a  27783  clwlkclwwlklem2  27785  clwlkclwwlkfo  27794  clwwisshclwwslemlem  27798  clwwlknwwlksn  27823  clwwlknlbonbgr1  27824  clwwlkn1loopb  27828  clwwlkf  27832  clwwlknon1  27882  clwwlknonwwlknonb  27891  clwwlknonex2lem2  27893  vdn0conngrumgrv2  27981  frgrnbnb  28078  frgrncvvdeqlem2  28085  frgrncvvdeqlem3  28086  frgrncvvdeqlem6  28089  frgrwopreglem4a  28095  fusgr2wsp2nb  28119  frrusgrord0lem  28124  numclwwlk2lem1lem  28127  2clwwlk2clwwlklem  28131  2clwwlk2clwwlk  28135  numclwwlk1lem2foa  28139  numclwwlk1lem2f1  28142  frgrreg  28179  hlipgt0  28697  ocin  29079  ocnel  29081  shmodsi  29172  pjmf1  29499  unopf1o  29699  staddi  30029  stadd3i  30031  mdi  30078  dmdmd  30083  dmdi  30085  dmdbr2  30086  dmdbr3  30088  dmdbr4  30089  dmdi4  30090  mdsl1i  30104  superpos  30137  cvbr4i  30150  atssma  30161  atcv1  30163  atomli  30165  chirredlem1  30173  addltmulALT  30229  bian1d  30230  ifeqeqx  30309  disjxpin  30351  suppss3  30486  fpwrelmap  30495  prmdvdsbc  30558  ogrpaddlt  30768  metider  31247  tpr2rico  31265  xrge0iifiso  31288  qqhcn  31342  qqhucn  31343  esumlub  31429  esumpinfval  31442  esumpinfsum  31446  ballotlemfc0  31860  ballotlemfcc  31861  ftc2re  31979  bnj517  32267  hashfundm  32464  fnrelpredd  32472  pfxwlk  32483  subgrwlk  32492  loop1cycl  32497  erdsze2lem2  32564  satfv1  32723  satfdmlem  32728  satf0op  32737  fmlasuc  32746  trpredrec  33190  poseq  33208  soseq  33209  sltval2  33276  sltres  33282  nodenselem8  33308  nodense  33309  noresle  33313  scutun12  33384  madeval2  33403  dfrdg4  33525  altopthsn  33535  btwncomim  33587  btwnexch3  33594  btwnexch2  33597  endofsegid  33659  opnrebl2  33782  nn0prpwlem  33783  onsuct0  33902  ordcmp  33908  nndivsub  33918  dnibndlem13  33942  bj-cbval  34095  bj-cbvex  34096  bj-cbvexw  34122  bj-cbv3tb  34224  bj-spimtv  34231  bj-equsal  34264  bj-sbsb  34275  bj-vtoclf  34355  bj-zfauscl  34367  currysetlem2  34383  bj-snsetex  34399  bj-ismooredr2  34525  bj-inftyexpiinj  34624  bj-finsumval0  34700  bj-fvimacnv0  34701  bj-bary1lem1  34725  bj-bary1  34726  f1omptsnlem  34753  iooelexlt  34779  relowlpssretop  34781  rdgeqoa  34787  finxpsuclem  34814  fvineqsneq  34829  pibt2  34834  wl-equsal1i  34948  wl-ax11-lem10  34991  ltflcei  35045  sin2h  35047  cos2h  35048  tan2h  35049  lindsenlbs  35052  matunitlindf  35055  poimirlem3  35060  poimirlem4  35061  poimirlem18  35075  poimirlem20  35077  poimirlem21  35078  poimirlem22  35079  poimirlem24  35081  poimirlem25  35082  poimirlem26  35083  poimirlem27  35084  poimirlem28  35085  poimirlem31  35088  poimir  35090  heicant  35092  mblfinlem1  35094  mblfinlem2  35095  mblfinlem3  35096  mblfinlem4  35097  mbfresfi  35103  cnambfre  35105  ftc1anc  35138  dvasin  35141  areacirclem1  35145  areacirclem4  35148  areacirc  35150  brabg2  35154  fzmul  35179  fdc  35183  incsequz2  35187  isbnd2  35221  opidonOLD  35290  opidon2OLD  35292  grpomndo  35313  elghomlem2OLD  35324  rngoueqz  35378  dvrunz  35392  divrngidl  35466  dral1-o  36200  lsatn0  36295  l1cvpat  36350  leat2  36590  atnle  36613  cvlcvr1  36635  cvrexchlem  36715  cvratlem  36717  cvrat  36718  atcvrj0  36724  atle  36732  snatpsubN  37046  linepsubN  37048  pmapsub  37064  lneq2at  37074  lncvrelatN  37077  2llnma3r  37084  cdlemblem  37089  paddasslem5  37120  poml4N  37249  lhpmcvr4N  37322  trlval2  37459  cdlemd6  37499  cdleme7ga  37544  cdleme25b  37650  cdleme29b  37671  cdleme35fnpq  37745  cdleme50f1  37839  cdlemf1  37857  cdlemg27b  37992  cdlemk28-3  38204  tendospcanN  38319  diaf11N  38345  dia2dimlem1  38360  dibf11N  38457  dihf11  38563  dihmeetlem1N  38586  dochvalr  38653  dochnel2  38688  dvh4dimlem  38739  dochsat0  38753  mapd1o  38944  hdmapf1oN  39161  hgmapval0  39188  hgmapf1oN  39199  hlhilhillem  39256  nnproddivdvdsd  39289  lcmineqlem  39340  metakunt7  39356  sn-axprlem3  39401  frlmsnic  39453  fsuppind  39456  oexpreposd  39487  rtprmirr  39502  prjspval  39597  rexrabdioph  39735  fphpdo  39758  irrapxlem3  39765  rmxypairf1o  39852  rmxycomplete  39858  zindbi  39887  lermxnn0  39891  ltrmy  39893  rmyeq0  39894  rmyeq  39895  lermy  39896  acongsym  39917  acongneg2  39918  wepwsolem  39986  intabssd  40227  iscard4  40241  ss2iundf  40360  frege129d  40464  frege133d  40466  axfrege52a  40557  axfrege52c  40588  ntrk0kbimka  40742  gneispace  40837  suprleubrd  40870  suprlubrd  40873  radcnvrat  41018  nzss  41021  expgrowthi  41037  ordpss  41155  bi23impib  41191  bi23imp13  41197  rspsbc2  41240  tratrb  41242  sbcim2g  41244  truniALT  41247  3impcombi  41523  tpid3gVD  41548  orbi1rVD  41554  sbc3orgVD  41557  rspsbc2VD  41561  tratrbVD  41567  sbcim2gVD  41581  sbcbiVD  41582  truniALTVD  41584  trintALTVD  41586  trintALT  41587  csbingVD  41590  csbsngVD  41599  csbxpgVD  41600  csbresgVD  41601  csbrngVD  41602  csbima12gALTVD  41603  csbunigVD  41604  csbfv12gALTVD  41605  relopabVD  41607  isosctrlem1ALT  41640  fzisoeu  41932  xrralrecnnge  42026  allbutfi  42029  climinf  42248  liminfreuzlem  42444  climliminf  42448  climliminflimsup  42450  xlimpnfxnegmnf  42456  xlimbr  42469  stoweidlem7  42649  stoweidlem62  42704  sge0gerpmpt  43041  meaiuninclem  43119  carageniuncllem2  43161  issmflem  43361  funressnfv  43635  funressnvmo  43637  2reu3  43666  ralbinrald  43678  afv0fv0  43705  afv0nbfvbi  43707  afvfv0bi  43708  fnbrafvb  43710  afvres  43728  tz6.12-afv  43729  afvco2  43732  ndmaovcl  43759  afv2res  43795  tz6.12-afv2  43796  nelbrim  43831  f1oresf1o2  43847  zm1nn  43859  nltle2tri  43870  subsubelfzo0  43883  iccpartres  43935  iccpartiltu  43939  fargshiftfv  43956  ichnreuop  43989  ichreuopeq  43990  prsprel  44004  sprsymrelf1lem  44008  sprsymrelfolem2  44010  sprsymrelfo  44014  prpair  44018  paireqne  44028  sbcpr  44038  fmtnof1  44052  goldbachthlem2  44063  fmtnoprmfac1  44082  fmtnoprmfac2  44084  lighneallem2  44124  lighneallem4b  44127  lighneallem4  44128  evennodd  44161  oddneven  44162  oexpnegnz  44196  evenltle  44235  fpprwppr  44257  fpprwpprb  44258  gbowge7  44281  gbege6  44283  sbgoldbwt  44295  sbgoldbst  44296  nnsum3primesle9  44312  bgoldbtbndlem2  44324  isomuspgrlem1  44345  isomuspgrlem2b  44347  isomuspgrlem2c  44348  isomuspgrlem2d  44349  mgmpropd  44395  clintop  44468  isassintop  44470  lidldomn1  44545  uzlidlring  44553  2zrngnmlid2  44575  rngccatidALTV  44613  ringccatidALTV  44676  srhmsubc  44700  srhmsubcALTV  44718  ztprmneprm  44749  pgrpgt2nabl  44768  lindslinindimp2lem4  44870  lincresunit3  44890  fldivexpfllog2  44979  digexp  45021  naryfvalelfv  45046  affinecomb1  45116  eenglngeehlnmlem1  45151  eenglngeehlnmlem2  45152  eenglngeehlnm  45153  itscnhlc0yqe  45173  itsclc0yqsol  45178  itscnhlc0xyqsol  45179  itschlc0xyqsol1  45180  itschlc0xyqsol  45181  itsclquadeu  45191  inlinecirc02plem  45200  inlinecirc02p  45201  spd  45208  spcdvw  45209  setrec2fun  45222