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  252  con4bid  316  mtbird  324  mtbiri  326  imbi1d  341  bitr3  352  pm5.21im  374  biimpa  477  alexbii  1835  spvv  2000  spfw  2036  cbvalw  2038  sbequi  2087  chvarfv  2233  cbvalv1  2337  spv  2392  chvar  2394  cbval  2397  sb1  2477  nfsb4t  2498  exmoeu  2575  euim  2613  2eu3  2649  eqrdav  2731  ralbida  3267  raleleqOLD  3340  rgen2a  3367  ralcom2  3373  ceqsalt  3505  ceqsalgALT  3508  vtoclfOLD  3548  vtoclegft  3573  spcdv  3584  rspcdv  3604  rspcebdv  3606  rexraleqim  3635  elabgtOLD  3663  sbcn1  3832  sbcim1OLD  3834  sbcbi1  3838  sbeqalb  3845  sbcel21v  3850  disj  4447  elpwunsn  4687  rabsnifsb  4726  ssunsn2  4830  preqr1g  4853  iuneqconst  5008  axprlem3  5423  sbcop1  5488  propeqop  5507  euotd  5513  rexopabb  5528  sotr2  5620  relop  5850  elinxp  6019  elimasni  6090  sotri2  6130  onmindif  6456  iotavalOLD  6517  dffv2  6986  mpteqb  7017  elfvmptrab  7026  chfnrn  7050  elpreima  7059  iinpreima  7070  exfo  7106  ffnfv  7117  f1elima  7261  f1eqcocnv  7298  f1eqcocnvOLD  7299  fliftfun  7308  soisores  7323  isotr  7332  isomin  7333  ovmpodv2  7565  difsnexi  7747  onint  7777  oneqmin  7787  ordunisuc2  7832  tfindsg  7849  findsg  7889  f1oweALT  7958  el2mpocl  8071  poseq  8143  soseq  8144  ressuppss  8167  funsssuppss  8174  suppofssd  8187  smoiso  8361  seqomlem2  8450  oaordi  8545  oawordri  8549  oaordex  8557  oalimcl  8559  omwordi  8570  oewordi  8590  oelim2  8594  nnmwordi  8634  xpider  8781  iiner  8782  undifixp  8927  mptelixpg  8928  dom2lem  8987  findcard2s  9164  pssnn  9167  nneneq  9208  nneneqOLD  9220  fineqvlem  9261  pssnnOLD  9264  dif1ennnALT  9276  unfilem2  9310  xpfiOLD  9317  domunfican  9319  f1dmvrnfibi  9335  fsuppimp  9367  dffi2  9417  infsupprpr  9498  wemaplem2  9541  suc11reg  9613  noinfep  9654  cantnflem1  9683  r1fin  9767  tcrank  9878  cardlim  9966  pr2nelemOLD  9997  fseqenlem1  10018  alephnbtwn  10065  alephord2i  10071  alephf1  10079  cardaleph  10083  alephiso  10092  dfac12lem2  10138  ackbij1lem16  10229  cflm  10244  cfcoflem  10266  sornom  10271  fin23lem27  10322  isf32lem7  10353  fin17  10388  fin1a2lem2  10395  fin1a2lem4  10397  fin1a2lem6  10399  fin1a2lem9  10402  axdc3lem2  10445  zorn2lem7  10496  uniimadom  10538  inar1  10769  grothomex  10823  addcanpi  10893  mulcanpi  10894  enqer  10915  genpcd  11000  genpnmax  11001  ltexprlem4  11033  reclem3pr  11043  reclem4pr  11044  suplem2pr  11047  axpre-ltadd  11161  axpre-sup  11163  ltletr  11305  00id  11388  addn0nid  11633  mul0or  11853  prodgt02  12061  lemul1a  12067  mulgt1  12072  divgt0  12081  divge0  12082  ledivp1i  12138  ltdivp1i  12139  cju  12207  nnsub  12255  nominpos  12448  nn0n0n1ge2  12538  btwnnz  12637  suprfinzcl  12675  ublbneg  12916  zmax  12928  cnref1o  12968  ltsubrp  13009  ltaddrp  13010  xrltletr  13135  qbtwnre  13177  xltnegi  13194  xnn0xadd0  13225  iccsupr  13418  icoshft  13449  difreicc  13460  iccshftri  13463  iccshftli  13465  iccdili  13467  icccntri  13469  fzen  13517  elfz1b  13569  fzofzim  13678  eluzgtdifelfzo  13693  elfzo1elm1fzo0  13732  injresinjlem  13751  injresinj  13752  flval2  13778  flval3  13779  modmuladdim  13878  modaddmodup  13898  addmodlteq  13910  fseqsupubi  13942  ssnn0fi  13949  mptnn0fsuppr  13963  sq01  14187  hashf1rn  14311  hashgt12el  14381  hashgt12el2  14382  hashfundm  14401  hash2pr  14429  hash2exprb  14431  hashge2el2difr  14441  hashtpg  14445  hash3tr  14450  lswlgt0cl  14518  ccatalpha  14542  pfxfv  14631  pfxsuff1eqwrdeq  14648  ccatopth2  14666  swrdccat  14684  swrdccat3blem  14688  reuccatpfxs1lem  14695  repsdf2  14727  repswsymball  14728  repswrevw  14736  cshweqrep  14770  cshw1  14771  2cshwcshw  14775  scshwfzeqfzo  14776  cshwcsh2id  14778  swrdco  14787  swrd2lsw  14902  2swrd2eqwrdeq  14903  wwlktovfo  14908  cjre  15085  icodiamlt  15381  reusq0  15408  o1lo1  15480  o1of2  15556  o1rlimmul  15562  zsum  15663  modfsummods  15738  zprod  15880  reeff1  16062  dvdsmod0  16202  dvds2lem  16211  muldvds1  16223  dvdscmulr  16227  dvdsmulcr  16228  dvdsdivcl  16258  mod2eq1n2dvds  16289  oddnn02np1  16290  divalglem8  16342  ndvdsadd  16352  zeqzmulgcd  16450  dfgcd2  16487  absproddvds  16553  lcmftp  16572  coprmdvds  16589  2mulprm  16629  isprm5  16643  divgcdodd  16646  isprm6  16650  prmdvdsexpr  16653  cncongrprm  16664  phiprmpw  16708  modprm0  16737  pythagtriplem4  16751  pcz  16813  difsqpwdvds  16819  1arith  16859  prmgaplem5  16987  prmgaplem6  16988  cshwrepswhash1  17035  sbcie2s  17093  divsfval  17492  catsubcat  17788  fthmon  17877  isinitoi  17948  istermoi  17949  iszeroi  17958  setcmon  18036  setcepi  18037  funcestrcsetclem8  18098  fthestrcsetc  18101  funcsetcestrclem8  18113  fthsetcestrc  18116  odupos  18280  pltnle  18290  pltval3  18291  lublecllem  18312  latasym  18395  mrelatglb  18512  mrelatlub  18514  cnvpsb  18531  isgrpid2  18860  ghmghmrn  19110  ghmf1  19120  orbsta  19176  resscntz  19196  gsmsymgrfixlem1  19294  gsmsymgreqlem2  19298  mndodcongi  19410  odf1  19429  lsmss1  19532  lsmss2  19534  efgredeu  19619  cntzcmnss  19708  imasabl  19743  lt6abl  19762  ablfaclem3  19956  ringinvnz1ne0  20111  kerf1ghm  20281  0ringnnzr  20301  lspsneq  20734  lspsneu  20735  lsmcv  20753  lidldvgen  20892  domnmuln0  20913  opprdomn  20918  domnchr  21083  znf1o  21106  zntoslem  21111  znfld  21115  cygznlem2a  21122  cygznlem3  21124  phlssphl  21211  islindf4  21392  uvcendim  21401  ply1scln0  21813  gsummoncoe1  21827  matvscl  21932  scmataddcl  22017  scmatsubcl  22018  scmatfo  22031  scmatghm  22034  maducoeval2  22141  slesolinv  22181  cramerimplem2  22185  cpmatelimp  22213  cpmatelimp2  22215  cpmatacl  22217  cpmatinvcl  22218  pm2mpf1  22300  cayhamlem1  22367  cayleyhamilton1  22393  0ntr  22574  islpi  22652  lmss  22801  cmpcld  22905  cmpfi  22911  1stcelcls  22964  comppfsc  23035  ptcnplem  23124  qtophmeo  23320  fbdmn0  23337  fbasrn  23387  elfm3  23453  fmfnfmlem4  23460  fclscf  23528  cnpfcf  23544  alexsubALTlem3  23552  tsmsres  23647  blval2  24070  tnggrpr  24171  nmoleub  24247  nmhmcn  24635  ncvs1  24673  iscau4  24795  caussi  24813  cmssmscld  24866  cmslssbn  24888  cniccbdd  24977  ovoliunnul  25023  mbfinf  25181  itg2splitlem  25265  dvcn  25437  c1lip1  25513  c1lip3  25515  dvcnvrelem1  25533  ply1divex  25653  quotcan  25821  aannenlem1  25840  taylf  25872  ulmcaulem  25905  ulmcau  25906  reeff1o  25958  logccv  26170  logreclem  26264  isosctrlem2  26321  xrlimcnp  26470  rlimcxp  26475  ftalem7  26580  vmappw  26617  fsumvma  26713  dchreq  26758  dchrptlem1  26764  dchrsum  26769  bposlem7  26790  lgsqrlem2  26847  lgsdchr  26855  gausslemma2dlem1a  26865  lgseisenlem2  26876  lgsquad2  26886  2lgslem1b  26892  2sqlem6  26923  2sqnn0  26938  addsq2reu  26940  2sqreulem2  26952  sltval2  27156  sltres  27162  nodenselem8  27191  nodense  27192  noresle  27197  scutun12  27308  madeval2  27345  elmade  27359  negsf1o  27525  recsex  27662  tgcgrcomimp  27725  isperp2  27963  xmstrkgc  28140  brbtwn  28154  brcgr  28155  axcgrid  28171  axeuclidlem  28217  axeuclid  28218  elntg2  28240  lpvtx  28325  upgrex  28349  upgrpredgv  28396  upgredgpr  28399  uhgr0v0e  28492  subgrprop  28527  fusgrfisbase  28582  edgnbusgreu  28621  nbusgredgeu0  28622  cusgredg  28678  structtocusgr  28700  cusgrsize2inds  28707  cusgrsize  28708  usgredgsscusgredg  28713  fusgrmaxsize  28718  uspgrloopvtxel  28770  umgr2v2e  28779  vtxdginducedm1fi  28798  finsumvtxdg2sstep  28803  rgrprop  28814  rusgrprop  28816  0uhgrrusgr  28832  rusgrpropedg  28838  ewlkprop  28857  upgrewlkle2  28860  wlkprop  28865  upgrwlkcompim  28897  uspgr2wlkeq  28900  wlklenvclwlk  28909  wlkonprop  28912  wlkres  28924  redwlk  28926  wlkdlem2  28937  wksonproplem  28958  wksonproplemOLD  28959  usgr2trlspth  29015  usgr2pth  29018  pthdlem1  29020  crctcshwlkn0lem4  29064  wwlksnprcl  29090  wlkiswwlks2  29126  wwlksm1edg  29132  wlknewwlksn  29138  wwlksnred  29143  wwlksnextbi  29145  wwlksnextwrd  29148  wwlksnextinj  29150  wwlksnextsurj  29151  umgr2wlk  29200  umgrwwlks2on  29208  elwwlks2  29217  clwwlk1loop  29238  umgrclwwlkge2  29241  clwlkclwwlklem2a1  29242  clwlkclwwlklem2a4  29247  clwlkclwwlklem2a  29248  clwlkclwwlklem2  29250  clwlkclwwlkfo  29259  clwwisshclwwslemlem  29263  clwwlknwwlksn  29288  clwwlknlbonbgr1  29289  clwwlkn1loopb  29293  clwwlkf  29297  clwwlknon1  29347  clwwlknonwwlknonb  29356  clwwlknonex2lem2  29358  vdn0conngrumgrv2  29446  frgrnbnb  29543  frgrncvvdeqlem2  29550  frgrncvvdeqlem3  29551  frgrncvvdeqlem6  29554  frgrwopreglem4a  29560  fusgr2wsp2nb  29584  frrusgrord0lem  29589  numclwwlk2lem1lem  29592  2clwwlk2clwwlklem  29596  2clwwlk2clwwlk  29600  numclwwlk1lem2foa  29604  numclwwlk1lem2f1  29607  frgrreg  29644  hlipgt0  30162  ocin  30544  ocnel  30546  shmodsi  30637  pjmf1  30964  unopf1o  31164  staddi  31494  stadd3i  31496  mdi  31543  dmdmd  31548  dmdi  31550  dmdbr2  31551  dmdbr3  31553  dmdbr4  31554  dmdi4  31555  mdsl1i  31569  superpos  31602  cvbr4i  31615  atssma  31626  atcv1  31628  atomli  31630  chirredlem1  31638  addltmulALT  31694  bian1d  31695  ifeqeqx  31769  disjxpin  31814  suppss3  31944  fpwrelmap  31953  prmdvdsbc  32017  ogrpaddlt  32230  qsfld  32607  ply1degltdimlem  32702  ply1degltdim  32703  metider  32869  tpr2rico  32887  xrge0iifiso  32910  qqhcn  32966  qqhucn  32967  esumlub  33053  esumpinfval  33066  esumpinfsum  33070  ballotlemfc0  33486  ballotlemfcc  33487  ftc2re  33605  bnj517  33891  fnrelpredd  34087  pfxwlk  34109  subgrwlk  34118  loop1cycl  34123  erdsze2lem2  34190  satfv1  34349  satfdmlem  34354  satf0op  34363  fmlasuc  34372  dfrdg4  34918  altopthsn  34928  btwncomim  34980  btwnexch3  34987  btwnexch2  34990  endofsegid  35052  gg-negcncf  35161  gg-dvfsumlem2  35178  opnrebl2  35201  nn0prpwlem  35202  onsuct0  35321  ordcmp  35327  nndivsub  35337  dnibndlem13  35361  bj-cbval  35521  bj-cbvex  35522  bj-cbvexw  35548  bj-cbv3tb  35660  bj-spimtv  35667  bj-equsal  35699  bj-sbsb  35710  bj-vtoclf  35790  bj-zfauscl  35799  bj-gabss  35810  bj-gabeqd  35812  currysetlem2  35824  bj-snsetex  35839  bj-ismooredr2  35986  bj-inftyexpiinj  36085  bj-finsumval0  36161  bj-fvimacnv0  36162  bj-bary1lem1  36187  bj-bary1  36188  f1omptsnlem  36212  iooelexlt  36238  relowlpssretop  36240  rdgeqoa  36246  finxpsuclem  36273  fvineqsneq  36288  pibt2  36293  wl-equsal1i  36407  wl-ax11-lem10  36451  ltflcei  36471  sin2h  36473  cos2h  36474  tan2h  36475  lindsenlbs  36478  matunitlindf  36481  poimirlem3  36486  poimirlem4  36487  poimirlem18  36501  poimirlem20  36503  poimirlem21  36504  poimirlem22  36505  poimirlem24  36507  poimirlem25  36508  poimirlem26  36509  poimirlem27  36510  poimirlem28  36511  poimirlem31  36514  poimir  36516  heicant  36518  mblfinlem1  36520  mblfinlem2  36521  mblfinlem3  36522  mblfinlem4  36523  mbfresfi  36529  cnambfre  36531  ftc1anc  36564  dvasin  36567  areacirclem1  36571  areacirclem4  36574  areacirc  36576  brabg2  36580  fzmul  36604  fdc  36608  incsequz2  36612  isbnd2  36646  opidonOLD  36715  opidon2OLD  36717  grpomndo  36738  elghomlem2OLD  36749  rngoueqz  36803  dvrunz  36817  divrngidl  36891  refressn  37308  dral1-o  37769  lsatn0  37864  l1cvpat  37919  leat2  38159  atnle  38182  cvlcvr1  38204  cvrexchlem  38285  cvratlem  38287  cvrat  38288  atcvrj0  38294  atle  38302  snatpsubN  38616  linepsubN  38618  pmapsub  38634  lneq2at  38644  lncvrelatN  38647  2llnma3r  38654  cdlemblem  38659  paddasslem5  38690  poml4N  38819  lhpmcvr4N  38892  trlval2  39029  cdlemd6  39069  cdleme7ga  39114  cdleme25b  39220  cdleme29b  39241  cdleme35fnpq  39315  cdleme50f1  39409  cdlemf1  39427  cdlemg27b  39562  cdlemk28-3  39774  tendospcanN  39889  diaf11N  39915  dia2dimlem1  39930  dibf11N  40027  dihf11  40133  dihmeetlem1N  40156  dochvalr  40223  dochnel2  40258  dvh4dimlem  40309  dochsat0  40323  mapd1o  40514  hdmapf1oN  40731  hgmapval0  40758  hgmapf1oN  40769  hlhilhillem  40830  nnproddivdvdsd  40861  lcmineqlem  40912  aks4d1p1p5  40935  aks4d1p3  40938  aks4d1p8d2  40945  aks4d1p8  40947  aks4d1p9  40948  fldhmf1  40950  aks6d1c2p2  40952  sticksstones1  40957  sticksstones3  40959  sticksstones8  40964  sticksstones11  40967  sticksstones12  40969  sticksstones20  40977  sticksstones22  40979  metakunt7  40986  sn-axprlem3  41036  frlmsnic  41112  fsuppind  41164  oexpreposd  41212  rtprmirr  41238  prjspval  41346  rexrabdioph  41522  fphpdo  41545  irrapxlem3  41552  rmxypairf1o  41640  rmxycomplete  41646  zindbi  41675  lermxnn0  41679  ltrmy  41681  rmyeq0  41682  rmyeq  41683  lermy  41684  acongsym  41705  acongneg2  41706  wepwsolem  41774  onsupuni  41968  onsupmaxb  41978  onsucf1o  42012  onov0suclim  42014  oe0suclim  42017  onsucwordi  42028  cantnfresb  42064  omabs2  42072  tfsconcat0b  42086  tfsconcatrev  42088  naddcnffo  42104  oaun3lem1  42114  oaltom  42146  omltoe  42148  sdomne0  42154  sdomne0d  42155  safesnsupfidom1o  42158  intabssd  42260  iscard4  42274  ss2iundf  42400  frege129d  42504  frege133d  42506  axfrege52a  42597  axfrege52c  42628  ntrk0kbimka  42780  gneispace  42875  suprleubrd  42908  suprlubrd  42910  radcnvrat  43063  nzss  43066  expgrowthi  43082  ordpss  43200  bi23impib  43236  bi23imp13  43242  rspsbc2  43285  tratrb  43287  sbcim2g  43289  truniALT  43292  3impcombi  43568  tpid3gVD  43593  orbi1rVD  43599  sbc3orgVD  43602  rspsbc2VD  43606  tratrbVD  43612  sbcim2gVD  43626  sbcbiVD  43627  truniALTVD  43629  trintALTVD  43631  trintALT  43632  csbingVD  43635  csbsngVD  43644  csbxpgVD  43645  csbresgVD  43646  csbrngVD  43647  csbima12gALTVD  43648  csbunigVD  43649  csbfv12gALTVD  43650  relopabVD  43652  isosctrlem1ALT  43685  fzisoeu  44000  xrralrecnnge  44090  allbutfi  44093  climinf  44312  liminfreuzlem  44508  climliminf  44512  climliminflimsup  44514  xlimpnfxnegmnf  44520  xlimbr  44533  stoweidlem7  44713  stoweidlem62  44768  sge0gerpmpt  45108  meaiuninclem  45186  carageniuncllem2  45228  issmflem  45433  et-sqrtnegnre  45579  natlocalincr  45580  tworepnotupword  45590  funressnfv  45743  funressnvmo  45745  f1cof1b  45775  2reu3  45808  ralbinrald  45820  afv0fv0  45847  afv0nbfvbi  45849  afvfv0bi  45850  fnbrafvb  45852  afvres  45870  tz6.12-afv  45871  afvco2  45874  ndmaovcl  45901  afv2res  45937  tz6.12-afv2  45938  nelbrim  45973  f1oresf1o2  45989  zm1nn  46000  nltle2tri  46011  subsubelfzo0  46024  iccpartres  46076  iccpartiltu  46080  fargshiftfv  46097  ichnreuop  46130  ichreuopeq  46131  prsprel  46145  sprsymrelf1lem  46149  sprsymrelfolem2  46151  sprsymrelfo  46155  prpair  46159  paireqne  46169  sbcpr  46179  fmtnof1  46193  goldbachthlem2  46204  fmtnoprmfac1  46223  fmtnoprmfac2  46225  lighneallem2  46264  lighneallem4b  46267  lighneallem4  46268  evennodd  46301  oddneven  46302  oexpnegnz  46336  evenltle  46375  fpprwppr  46397  fpprwpprb  46398  gbowge7  46421  gbege6  46423  sbgoldbwt  46435  sbgoldbst  46436  nnsum3primesle9  46452  bgoldbtbndlem2  46464  isomuspgrlem1  46485  isomuspgrlem2b  46487  isomuspgrlem2c  46488  isomuspgrlem2d  46489  mgmpropd  46535  clintop  46608  isassintop  46610  subrngringnsg  46722  rnglidlmcl  46738  rngqiprngimf1lem  46769  lidldomn1  46813  uzlidlring  46817  2zrngnmlid2  46839  rngccatidALTV  46877  ringccatidALTV  46940  srhmsubc  46964  srhmsubcALTV  46982  ztprmneprm  47013  pgrpgt2nabl  47032  lindslinindimp2lem4  47132  lincresunit3  47152  fldivexpfllog2  47241  digexp  47283  naryfvalelfv  47308  affinecomb1  47378  eenglngeehlnmlem1  47413  eenglngeehlnmlem2  47414  eenglngeehlnm  47415  itscnhlc0yqe  47435  itsclc0yqsol  47440  itscnhlc0xyqsol  47441  itschlc0xyqsol1  47442  itschlc0xyqsol  47443  itsclquadeu  47453  inlinecirc02plem  47462  inlinecirc02p  47463  pm4.71da  47465  mofsn  47500  seposep  47548  idmon  47626  idepi  47627  prsthinc  47664  grptcmon  47706  grptcepi  47707  spd  47713  spcdvw  47714  setrec2fun  47727