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  imbitrid  243  syl6bi  253  con4bid  317  mtbird  325  mtbiri  327  imbi1d  342  bitr3  353  pm5.21im  375  biimpa  478  alexbii  1836  spvv  2001  spfw  2037  cbvalw  2039  sbequi  2088  chvarfv  2234  cbvalv1  2338  spv  2393  chvar  2395  cbval  2398  sb1  2478  nfsb4t  2499  exmoeu  2576  euim  2614  2eu3  2650  eqrdav  2732  ralbida  3268  raleleqOLD  3341  rgen2a  3368  ralcom2  3374  ceqsalt  3506  ceqsalgALT  3509  vtoclfOLD  3549  vtoclegft  3574  spcdv  3585  rspcdv  3605  rspcebdv  3607  rexraleqim  3636  elabgtOLD  3664  sbcn1  3833  sbcim1OLD  3835  sbcbi1  3839  sbeqalb  3846  sbcel21v  3851  disj  4448  elpwunsn  4688  rabsnifsb  4727  ssunsn2  4831  preqr1g  4854  iuneqconst  5009  axprlem3  5424  sbcop1  5489  propeqop  5508  euotd  5514  rexopabb  5529  sotr2  5621  relop  5851  elinxp  6020  elimasni  6091  sotri2  6131  onmindif  6457  iotavalOLD  6518  dffv2  6987  mpteqb  7018  elfvmptrab  7027  chfnrn  7051  elpreima  7060  iinpreima  7071  exfo  7107  ffnfv  7118  f1elima  7262  f1eqcocnv  7299  f1eqcocnvOLD  7300  fliftfun  7309  soisores  7324  isotr  7333  isomin  7334  ovmpodv2  7566  difsnexi  7748  onint  7778  oneqmin  7788  ordunisuc2  7833  tfindsg  7850  findsg  7890  f1oweALT  7959  el2mpocl  8072  poseq  8144  soseq  8145  ressuppss  8168  funsssuppss  8175  suppofssd  8188  smoiso  8362  seqomlem2  8451  oaordi  8546  oawordri  8550  oaordex  8558  oalimcl  8560  omwordi  8571  oewordi  8591  oelim2  8595  nnmwordi  8635  xpider  8782  iiner  8783  undifixp  8928  mptelixpg  8929  dom2lem  8988  findcard2s  9165  pssnn  9168  nneneq  9209  nneneqOLD  9221  fineqvlem  9262  pssnnOLD  9265  dif1ennnALT  9277  unfilem2  9311  xpfiOLD  9318  domunfican  9320  f1dmvrnfibi  9336  fsuppimp  9368  dffi2  9418  infsupprpr  9499  wemaplem2  9542  suc11reg  9614  noinfep  9655  cantnflem1  9684  r1fin  9768  tcrank  9879  cardlim  9967  pr2nelemOLD  9998  fseqenlem1  10019  alephnbtwn  10066  alephord2i  10072  alephf1  10080  cardaleph  10084  alephiso  10093  dfac12lem2  10139  ackbij1lem16  10230  cflm  10245  cfcoflem  10267  sornom  10272  fin23lem27  10323  isf32lem7  10354  fin17  10389  fin1a2lem2  10396  fin1a2lem4  10398  fin1a2lem6  10400  fin1a2lem9  10403  axdc3lem2  10446  zorn2lem7  10497  uniimadom  10539  inar1  10770  grothomex  10824  addcanpi  10894  mulcanpi  10895  enqer  10916  genpcd  11001  genpnmax  11002  ltexprlem4  11034  reclem3pr  11044  reclem4pr  11045  suplem2pr  11048  axpre-ltadd  11162  axpre-sup  11164  ltletr  11306  00id  11389  addn0nid  11634  mul0or  11854  prodgt02  12062  lemul1a  12068  mulgt1  12073  divgt0  12082  divge0  12083  ledivp1i  12139  ltdivp1i  12140  cju  12208  nnsub  12256  nominpos  12449  nn0n0n1ge2  12539  btwnnz  12638  suprfinzcl  12676  ublbneg  12917  zmax  12929  cnref1o  12969  ltsubrp  13010  ltaddrp  13011  xrltletr  13136  qbtwnre  13178  xltnegi  13195  xnn0xadd0  13226  iccsupr  13419  icoshft  13450  difreicc  13461  iccshftri  13464  iccshftli  13466  iccdili  13468  icccntri  13470  fzen  13518  elfz1b  13570  fzofzim  13679  eluzgtdifelfzo  13694  elfzo1elm1fzo0  13733  injresinjlem  13752  injresinj  13753  flval2  13779  flval3  13780  modmuladdim  13879  modaddmodup  13899  addmodlteq  13911  fseqsupubi  13943  ssnn0fi  13950  mptnn0fsuppr  13964  sq01  14188  hashf1rn  14312  hashgt12el  14382  hashgt12el2  14383  hashfundm  14402  hash2pr  14430  hash2exprb  14432  hashge2el2difr  14442  hashtpg  14446  hash3tr  14451  lswlgt0cl  14519  ccatalpha  14543  pfxfv  14632  pfxsuff1eqwrdeq  14649  ccatopth2  14667  swrdccat  14685  swrdccat3blem  14689  reuccatpfxs1lem  14696  repsdf2  14728  repswsymball  14729  repswrevw  14737  cshweqrep  14771  cshw1  14772  2cshwcshw  14776  scshwfzeqfzo  14777  cshwcsh2id  14779  swrdco  14788  swrd2lsw  14903  2swrd2eqwrdeq  14904  wwlktovfo  14909  cjre  15086  icodiamlt  15382  reusq0  15409  o1lo1  15481  o1of2  15557  o1rlimmul  15563  zsum  15664  modfsummods  15739  zprod  15881  reeff1  16063  dvdsmod0  16203  dvds2lem  16212  muldvds1  16224  dvdscmulr  16228  dvdsmulcr  16229  dvdsdivcl  16259  mod2eq1n2dvds  16290  oddnn02np1  16291  divalglem8  16343  ndvdsadd  16353  zeqzmulgcd  16451  dfgcd2  16488  absproddvds  16554  lcmftp  16573  coprmdvds  16590  2mulprm  16630  isprm5  16644  divgcdodd  16647  isprm6  16651  prmdvdsexpr  16654  cncongrprm  16665  phiprmpw  16709  modprm0  16738  pythagtriplem4  16752  pcz  16814  difsqpwdvds  16820  1arith  16860  prmgaplem5  16988  prmgaplem6  16989  cshwrepswhash1  17036  sbcie2s  17094  divsfval  17493  catsubcat  17789  fthmon  17878  isinitoi  17949  istermoi  17950  iszeroi  17959  setcmon  18037  setcepi  18038  funcestrcsetclem8  18099  fthestrcsetc  18102  funcsetcestrclem8  18114  fthsetcestrc  18117  odupos  18281  pltnle  18291  pltval3  18292  lublecllem  18313  latasym  18396  mrelatglb  18513  mrelatlub  18515  cnvpsb  18532  isgrpid2  18861  ghmghmrn  19111  ghmf1  19121  orbsta  19177  resscntz  19197  gsmsymgrfixlem1  19295  gsmsymgreqlem2  19299  mndodcongi  19411  odf1  19430  lsmss1  19533  lsmss2  19535  efgredeu  19620  cntzcmnss  19709  imasabl  19744  lt6abl  19763  ablfaclem3  19957  ringinvnz1ne0  20112  kerf1ghm  20282  0ringnnzr  20302  lspsneq  20735  lspsneu  20736  lsmcv  20754  lidldvgen  20893  domnmuln0  20914  opprdomn  20919  domnchr  21084  znf1o  21107  zntoslem  21112  znfld  21116  cygznlem2a  21123  cygznlem3  21125  phlssphl  21212  islindf4  21393  uvcendim  21402  ply1scln0  21814  gsummoncoe1  21828  matvscl  21933  scmataddcl  22018  scmatsubcl  22019  scmatfo  22032  scmatghm  22035  maducoeval2  22142  slesolinv  22182  cramerimplem2  22186  cpmatelimp  22214  cpmatelimp2  22216  cpmatacl  22218  cpmatinvcl  22219  pm2mpf1  22301  cayhamlem1  22368  cayleyhamilton1  22394  0ntr  22575  islpi  22653  lmss  22802  cmpcld  22906  cmpfi  22912  1stcelcls  22965  comppfsc  23036  ptcnplem  23125  qtophmeo  23321  fbdmn0  23338  fbasrn  23388  elfm3  23454  fmfnfmlem4  23461  fclscf  23529  cnpfcf  23545  alexsubALTlem3  23553  tsmsres  23648  blval2  24071  tnggrpr  24172  nmoleub  24248  nmhmcn  24636  ncvs1  24674  iscau4  24796  caussi  24814  cmssmscld  24867  cmslssbn  24889  cniccbdd  24978  ovoliunnul  25024  mbfinf  25182  itg2splitlem  25266  dvcn  25438  c1lip1  25514  c1lip3  25516  dvcnvrelem1  25534  ply1divex  25654  quotcan  25822  aannenlem1  25841  taylf  25873  ulmcaulem  25906  ulmcau  25907  reeff1o  25959  logccv  26171  logreclem  26267  isosctrlem2  26324  xrlimcnp  26473  rlimcxp  26478  ftalem7  26583  vmappw  26620  fsumvma  26716  dchreq  26761  dchrptlem1  26767  dchrsum  26772  bposlem7  26793  lgsqrlem2  26850  lgsdchr  26858  gausslemma2dlem1a  26868  lgseisenlem2  26879  lgsquad2  26889  2lgslem1b  26895  2sqlem6  26926  2sqnn0  26941  addsq2reu  26943  2sqreulem2  26955  sltval2  27159  sltres  27165  nodenselem8  27194  nodense  27195  noresle  27200  scutun12  27312  madeval2  27349  elmade  27363  negsf1o  27531  recsex  27668  tgcgrcomimp  27759  isperp2  27997  xmstrkgc  28174  brbtwn  28188  brcgr  28189  axcgrid  28205  axeuclidlem  28251  axeuclid  28252  elntg2  28274  lpvtx  28359  upgrex  28383  upgrpredgv  28430  upgredgpr  28433  uhgr0v0e  28526  subgrprop  28561  fusgrfisbase  28616  edgnbusgreu  28655  nbusgredgeu0  28656  cusgredg  28712  structtocusgr  28734  cusgrsize2inds  28741  cusgrsize  28742  usgredgsscusgredg  28747  fusgrmaxsize  28752  uspgrloopvtxel  28804  umgr2v2e  28813  vtxdginducedm1fi  28832  finsumvtxdg2sstep  28837  rgrprop  28848  rusgrprop  28850  0uhgrrusgr  28866  rusgrpropedg  28872  ewlkprop  28891  upgrewlkle2  28894  wlkprop  28899  upgrwlkcompim  28931  uspgr2wlkeq  28934  wlklenvclwlk  28943  wlkonprop  28946  wlkres  28958  redwlk  28960  wlkdlem2  28971  wksonproplem  28992  wksonproplemOLD  28993  usgr2trlspth  29049  usgr2pth  29052  pthdlem1  29054  crctcshwlkn0lem4  29098  wwlksnprcl  29124  wlkiswwlks2  29160  wwlksm1edg  29166  wlknewwlksn  29172  wwlksnred  29177  wwlksnextbi  29179  wwlksnextwrd  29182  wwlksnextinj  29184  wwlksnextsurj  29185  umgr2wlk  29234  umgrwwlks2on  29242  elwwlks2  29251  clwwlk1loop  29272  umgrclwwlkge2  29275  clwlkclwwlklem2a1  29276  clwlkclwwlklem2a4  29281  clwlkclwwlklem2a  29282  clwlkclwwlklem2  29284  clwlkclwwlkfo  29293  clwwisshclwwslemlem  29297  clwwlknwwlksn  29322  clwwlknlbonbgr1  29323  clwwlkn1loopb  29327  clwwlkf  29331  clwwlknon1  29381  clwwlknonwwlknonb  29390  clwwlknonex2lem2  29392  vdn0conngrumgrv2  29480  frgrnbnb  29577  frgrncvvdeqlem2  29584  frgrncvvdeqlem3  29585  frgrncvvdeqlem6  29588  frgrwopreglem4a  29594  fusgr2wsp2nb  29618  frrusgrord0lem  29623  numclwwlk2lem1lem  29626  2clwwlk2clwwlklem  29630  2clwwlk2clwwlk  29634  numclwwlk1lem2foa  29638  numclwwlk1lem2f1  29641  frgrreg  29678  hlipgt0  30198  ocin  30580  ocnel  30582  shmodsi  30673  pjmf1  31000  unopf1o  31200  staddi  31530  stadd3i  31532  mdi  31579  dmdmd  31584  dmdi  31586  dmdbr2  31587  dmdbr3  31589  dmdbr4  31590  dmdi4  31591  mdsl1i  31605  superpos  31638  cvbr4i  31651  atssma  31662  atcv1  31664  atomli  31666  chirredlem1  31674  addltmulALT  31730  bian1d  31731  ifeqeqx  31805  disjxpin  31850  suppss3  31980  fpwrelmap  31989  prmdvdsbc  32053  ogrpaddlt  32266  qsfld  32643  ply1degltdimlem  32738  ply1degltdim  32739  metider  32905  tpr2rico  32923  xrge0iifiso  32946  qqhcn  33002  qqhucn  33003  esumlub  33089  esumpinfval  33102  esumpinfsum  33106  ballotlemfc0  33522  ballotlemfcc  33523  ftc2re  33641  bnj517  33927  fnrelpredd  34123  pfxwlk  34145  subgrwlk  34154  loop1cycl  34159  erdsze2lem2  34226  satfv1  34385  satfdmlem  34390  satf0op  34399  fmlasuc  34408  dfrdg4  34954  altopthsn  34964  btwncomim  35016  btwnexch3  35023  btwnexch2  35026  endofsegid  35088  gg-dvfsumlem2  35214  gg-cncrng  35231  gg-cnfld1  35232  opnrebl2  35254  nn0prpwlem  35255  onsuct0  35374  ordcmp  35380  nndivsub  35390  dnibndlem13  35414  bj-cbval  35574  bj-cbvex  35575  bj-cbvexw  35601  bj-cbv3tb  35713  bj-spimtv  35720  bj-equsal  35752  bj-sbsb  35763  bj-vtoclf  35843  bj-zfauscl  35852  bj-gabss  35863  bj-gabeqd  35865  currysetlem2  35877  bj-snsetex  35892  bj-ismooredr2  36039  bj-inftyexpiinj  36138  bj-finsumval0  36214  bj-fvimacnv0  36215  bj-bary1lem1  36240  bj-bary1  36241  f1omptsnlem  36265  iooelexlt  36291  relowlpssretop  36293  rdgeqoa  36299  finxpsuclem  36326  fvineqsneq  36341  pibt2  36346  wl-equsal1i  36460  wl-ax11-lem10  36504  ltflcei  36524  sin2h  36526  cos2h  36527  tan2h  36528  lindsenlbs  36531  matunitlindf  36534  poimirlem3  36539  poimirlem4  36540  poimirlem18  36554  poimirlem20  36556  poimirlem21  36557  poimirlem22  36558  poimirlem24  36560  poimirlem25  36561  poimirlem26  36562  poimirlem27  36563  poimirlem28  36564  poimirlem31  36567  poimir  36569  heicant  36571  mblfinlem1  36573  mblfinlem2  36574  mblfinlem3  36575  mblfinlem4  36576  mbfresfi  36582  cnambfre  36584  ftc1anc  36617  dvasin  36620  areacirclem1  36624  areacirclem4  36627  areacirc  36629  brabg2  36633  fzmul  36657  fdc  36661  incsequz2  36665  isbnd2  36699  opidonOLD  36768  opidon2OLD  36770  grpomndo  36791  elghomlem2OLD  36802  rngoueqz  36856  dvrunz  36870  divrngidl  36944  refressn  37361  dral1-o  37822  lsatn0  37917  l1cvpat  37972  leat2  38212  atnle  38235  cvlcvr1  38257  cvrexchlem  38338  cvratlem  38340  cvrat  38341  atcvrj0  38347  atle  38355  snatpsubN  38669  linepsubN  38671  pmapsub  38687  lneq2at  38697  lncvrelatN  38700  2llnma3r  38707  cdlemblem  38712  paddasslem5  38743  poml4N  38872  lhpmcvr4N  38945  trlval2  39082  cdlemd6  39122  cdleme7ga  39167  cdleme25b  39273  cdleme29b  39294  cdleme35fnpq  39368  cdleme50f1  39462  cdlemf1  39480  cdlemg27b  39615  cdlemk28-3  39827  tendospcanN  39942  diaf11N  39968  dia2dimlem1  39983  dibf11N  40080  dihf11  40186  dihmeetlem1N  40209  dochvalr  40276  dochnel2  40311  dvh4dimlem  40362  dochsat0  40376  mapd1o  40567  hdmapf1oN  40784  hgmapval0  40811  hgmapf1oN  40822  hlhilhillem  40883  nnproddivdvdsd  40914  lcmineqlem  40965  aks4d1p1p5  40988  aks4d1p3  40991  aks4d1p8d2  40998  aks4d1p8  41000  aks4d1p9  41001  fldhmf1  41003  aks6d1c2p2  41005  sticksstones1  41010  sticksstones3  41012  sticksstones8  41017  sticksstones11  41020  sticksstones12  41022  sticksstones20  41030  sticksstones22  41032  metakunt7  41039  sn-axprlem3  41082  frlmsnic  41158  fsuppind  41210  oexpreposd  41260  rtprmirr  41285  prjspval  41393  rexrabdioph  41580  fphpdo  41603  irrapxlem3  41610  rmxypairf1o  41698  rmxycomplete  41704  zindbi  41733  lermxnn0  41737  ltrmy  41739  rmyeq0  41740  rmyeq  41741  lermy  41742  acongsym  41763  acongneg2  41764  wepwsolem  41832  onsupuni  42026  onsupmaxb  42036  onsucf1o  42070  onov0suclim  42072  oe0suclim  42075  onsucwordi  42086  cantnfresb  42122  omabs2  42130  tfsconcat0b  42144  tfsconcatrev  42146  naddcnffo  42162  oaun3lem1  42172  oaltom  42204  omltoe  42206  sdomne0  42212  sdomne0d  42213  safesnsupfidom1o  42216  intabssd  42318  iscard4  42332  ss2iundf  42458  frege129d  42562  frege133d  42564  axfrege52a  42655  axfrege52c  42686  ntrk0kbimka  42838  gneispace  42933  suprleubrd  42966  suprlubrd  42968  radcnvrat  43121  nzss  43124  expgrowthi  43140  ordpss  43258  bi23impib  43294  bi23imp13  43300  rspsbc2  43343  tratrb  43345  sbcim2g  43347  truniALT  43350  3impcombi  43626  tpid3gVD  43651  orbi1rVD  43657  sbc3orgVD  43660  rspsbc2VD  43664  tratrbVD  43670  sbcim2gVD  43684  sbcbiVD  43685  truniALTVD  43687  trintALTVD  43689  trintALT  43690  csbingVD  43693  csbsngVD  43702  csbxpgVD  43703  csbresgVD  43704  csbrngVD  43705  csbima12gALTVD  43706  csbunigVD  43707  csbfv12gALTVD  43708  relopabVD  43710  isosctrlem1ALT  43743  fzisoeu  44058  xrralrecnnge  44148  allbutfi  44151  climinf  44370  liminfreuzlem  44566  climliminf  44570  climliminflimsup  44572  xlimpnfxnegmnf  44578  xlimbr  44591  stoweidlem7  44771  stoweidlem62  44826  sge0gerpmpt  45166  meaiuninclem  45244  carageniuncllem2  45286  issmflem  45491  et-sqrtnegnre  45637  natlocalincr  45638  tworepnotupword  45648  funressnfv  45801  funressnvmo  45803  f1cof1b  45833  2reu3  45866  ralbinrald  45878  afv0fv0  45905  afv0nbfvbi  45907  afvfv0bi  45908  fnbrafvb  45910  afvres  45928  tz6.12-afv  45929  afvco2  45932  ndmaovcl  45959  afv2res  45995  tz6.12-afv2  45996  nelbrim  46031  f1oresf1o2  46047  zm1nn  46058  nltle2tri  46069  subsubelfzo0  46082  iccpartres  46134  iccpartiltu  46138  fargshiftfv  46155  ichnreuop  46188  ichreuopeq  46189  prsprel  46203  sprsymrelf1lem  46207  sprsymrelfolem2  46209  sprsymrelfo  46213  prpair  46217  paireqne  46227  sbcpr  46237  fmtnof1  46251  goldbachthlem2  46262  fmtnoprmfac1  46281  fmtnoprmfac2  46283  lighneallem2  46322  lighneallem4b  46325  lighneallem4  46326  evennodd  46359  oddneven  46360  oexpnegnz  46394  evenltle  46433  fpprwppr  46455  fpprwpprb  46456  gbowge7  46479  gbege6  46481  sbgoldbwt  46493  sbgoldbst  46494  nnsum3primesle9  46510  bgoldbtbndlem2  46522  isomuspgrlem1  46543  isomuspgrlem2b  46545  isomuspgrlem2c  46546  isomuspgrlem2d  46547  mgmpropd  46593  clintop  46666  isassintop  46668  subrngringnsg  46780  rnglidlmcl  46796  rngqiprngimf1lem  46827  lidldomn1  46871  uzlidlring  46875  2zrngnmlid2  46897  rngccatidALTV  46935  ringccatidALTV  46998  srhmsubc  47022  srhmsubcALTV  47040  ztprmneprm  47071  pgrpgt2nabl  47090  lindslinindimp2lem4  47190  lincresunit3  47210  fldivexpfllog2  47299  digexp  47341  naryfvalelfv  47366  affinecomb1  47436  eenglngeehlnmlem1  47471  eenglngeehlnmlem2  47472  eenglngeehlnm  47473  itscnhlc0yqe  47493  itsclc0yqsol  47498  itscnhlc0xyqsol  47499  itschlc0xyqsol1  47500  itschlc0xyqsol  47501  itsclquadeu  47511  inlinecirc02plem  47520  inlinecirc02p  47521  pm4.71da  47523  mofsn  47558  seposep  47606  idmon  47684  idepi  47685  prsthinc  47722  grptcmon  47764  grptcepi  47765  spd  47771  spcdvw  47772  setrec2fun  47785