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  biimtrdi  252  con4bid  316  mtbird  324  mtbiri  326  imbi1d  340  bitr3  351  pm5.21im  373  biimpa  475  alexbii  1828  spvv  1993  spfw  2029  cbvalw  2031  sbequi  2080  chvarfv  2229  cbvalv1  2332  spv  2387  chvar  2389  cbval  2392  sb1  2472  nfsb4t  2493  exmoeu  2570  euim  2606  2eu3  2643  eqrdav  2725  ralbida  3258  rgen2a  3355  ralcom2  3361  ceqsalt  3496  ceqsalgALT  3499  vtoclfOLD  3545  vtoclegft  3569  spcdv  3579  rspcdv  3599  rspcebdv  3601  rexraleqim  3631  elabgtOLDOLD  3660  sbcn1  3831  sbcim1OLD  3833  sbcbi1  3837  sbeqalb  3843  sbcel21v  3848  disj  4444  elpwunsn  4682  rabsnifsb  4721  ssunsn2  4826  preqr1g  4851  iuneqconst  5004  axprlem3  5421  sbcop1  5486  propeqop  5505  euotd  5511  rexopabb  5526  sotr2  5618  relop  5849  elinxp  6020  elimasni  6093  sotri2  6133  onmindif  6460  iotavalOLD  6520  dffv2  6989  mpteqb  7020  elfvmptrab  7030  chfnrn  7054  elpreima  7063  iinpreima  7074  exfo  7111  ffnfv  7125  f1elima  7270  f1eqcocnv  7307  fliftfun  7316  soisores  7331  isotr  7340  isomin  7341  ovmpodv2  7576  difsnexi  7761  onint  7791  oneqmin  7801  ordunisuc2  7846  tfindsg  7863  findsg  7902  f1oweALT  7978  el2mpocl  8092  poseq  8164  soseq  8165  ressuppss  8189  funsssuppss  8196  suppofssd  8210  smoiso  8384  seqomlem2  8473  oaordi  8568  oawordri  8572  oaordex  8580  oalimcl  8582  omwordi  8593  oewordi  8613  oelim2  8617  nnmwordi  8657  xpider  8809  iiner  8810  undifixp  8955  mptelixpg  8956  dom2lem  9015  findcard2s  9195  pssnn  9198  nneneq  9236  nneneqOLD  9248  fineqvlem  9289  pssnnOLD  9292  dif1ennnALT  9304  unfilem2  9338  xpfiOLD  9354  domunfican  9356  f1dmvrnfibi  9376  fsuppimp  9405  dffi2  9459  infsupprpr  9540  wemaplem2  9583  suc11reg  9655  noinfep  9696  cantnflem1  9725  r1fin  9809  tcrank  9920  cardlim  10008  pr2nelemOLD  10039  fseqenlem1  10060  alephnbtwn  10107  alephord2i  10113  alephf1  10121  cardaleph  10125  alephiso  10134  dfac12lem2  10180  ackbij1lem16  10269  cflm  10284  cfcoflem  10306  sornom  10311  fin23lem27  10362  isf32lem7  10393  fin17  10428  fin1a2lem2  10435  fin1a2lem4  10437  fin1a2lem6  10439  fin1a2lem9  10442  axdc3lem2  10485  zorn2lem7  10536  uniimadom  10578  inar1  10809  grothomex  10863  addcanpi  10933  mulcanpi  10934  enqer  10955  genpcd  11040  genpnmax  11041  ltexprlem4  11073  reclem3pr  11083  reclem4pr  11084  suplem2pr  11087  axpre-ltadd  11201  axpre-sup  11203  ltletr  11347  00id  11430  addn0nid  11675  mul0or  11895  prodgt02  12107  lemul1a  12113  mulgt1OLD  12118  divgt0  12128  divge0  12129  ledivp1i  12185  ltdivp1i  12186  cju  12254  nnsub  12302  nominpos  12495  nn0n0n1ge2  12585  btwnnz  12684  suprfinzcl  12722  ublbneg  12963  zmax  12975  cnref1o  13015  ltsubrp  13058  ltaddrp  13059  xrltletr  13184  qbtwnre  13226  xltnegi  13243  xnn0xadd0  13274  iccsupr  13467  icoshft  13498  difreicc  13509  iccshftri  13512  iccshftli  13514  iccdili  13516  icccntri  13518  fzen  13566  elfz1b  13618  fzofzim  13727  eluzgtdifelfzo  13742  elfzo1elm1fzo0  13782  injresinjlem  13801  injresinj  13802  flval2  13828  flval3  13829  modmuladdim  13928  modaddmodup  13948  addmodlteq  13960  fseqsupubi  13992  ssnn0fi  13999  mptnn0fsuppr  14013  sq01  14237  hashf1rn  14364  hashgt12el  14434  hashgt12el2  14435  hashfundm  14454  hash2pr  14483  hash2exprb  14485  hashge2el2difr  14495  hashtpg  14499  hash3tr  14504  lswlgt0cl  14572  ccatalpha  14596  pfxfv  14685  pfxsuff1eqwrdeq  14702  ccatopth2  14720  swrdccat  14738  swrdccat3blem  14742  reuccatpfxs1lem  14749  repsdf2  14781  repswsymball  14782  repswrevw  14790  cshweqrep  14824  cshw1  14825  2cshwcshw  14829  scshwfzeqfzo  14830  cshwcsh2id  14832  swrdco  14841  swrd2lsw  14956  2swrd2eqwrdeq  14957  wwlktovfo  14962  cjre  15139  icodiamlt  15435  reusq0  15462  o1lo1  15534  o1of2  15610  o1rlimmul  15616  zsum  15717  modfsummods  15792  zprod  15934  reeff1  16117  dvdsmod0  16257  dvds2lem  16266  muldvds1  16278  dvdscmulr  16282  dvdsmulcr  16283  dvdsdivcl  16313  mod2eq1n2dvds  16344  oddnn02np1  16345  divalglem8  16397  ndvdsadd  16407  zeqzmulgcd  16505  dfgcd2  16542  absproddvds  16613  lcmftp  16632  coprmdvds  16649  2mulprm  16689  isprm5  16703  divgcdodd  16706  isprm6  16710  prmdvdsexpr  16713  prmdvdsbc  16723  cncongrprm  16726  phiprmpw  16773  modprm0  16802  pythagtriplem4  16816  pcz  16878  difsqpwdvds  16884  1arith  16924  prmgaplem5  17052  prmgaplem6  17053  cshwrepswhash1  17100  sbcie2s  17158  divsfval  17557  catsubcat  17853  fthmon  17944  isinitoi  18016  istermoi  18017  iszeroi  18026  setcmon  18104  setcepi  18105  funcestrcsetclem8  18166  fthestrcsetc  18169  funcsetcestrclem8  18181  fthsetcestrc  18184  odupos  18348  pltnle  18358  pltval3  18359  lublecllem  18380  latasym  18463  mrelatglb  18580  mrelatlub  18582  cnvpsb  18599  mgmpropd  18639  isgrpid2  18966  ghmghmrn  19225  ghmf1  19236  kerf1ghm  19237  orbsta  19303  resscntz  19323  gsmsymgrfixlem1  19421  gsmsymgreqlem2  19425  mndodcongi  19537  odf1  19556  lsmss1  19659  lsmss2  19661  efgredeu  19746  cntzcmnss  19835  imasabl  19870  lt6abl  19889  ablfaclem3  20083  ringinvnz1ne0  20275  0ringnnzr  20503  subrngringnsg  20531  srhmsubc  20654  domnmuln0  20683  lspsneq  21099  lspsneu  21100  lsmcv  21118  rnglidlmcl  21201  rngqiprngimf1lem  21279  lidldvgen  21319  domnchr  21522  znf1o  21545  zntoslem  21550  znfld  21554  cygznlem2a  21561  cygznlem3  21563  phlssphl  21651  islindf4  21832  uvcendim  21841  psdmul  22156  ply1scln0  22279  gsummoncoe1  22296  matvscl  22421  scmataddcl  22506  scmatsubcl  22507  scmatfo  22520  scmatghm  22523  maducoeval2  22630  slesolinv  22670  cramerimplem2  22674  cpmatelimp  22702  cpmatelimp2  22704  cpmatacl  22706  cpmatinvcl  22707  pm2mpf1  22789  cayhamlem1  22856  cayleyhamilton1  22882  0ntr  23063  islpi  23141  lmss  23290  cmpcld  23394  cmpfi  23400  1stcelcls  23453  comppfsc  23524  ptcnplem  23613  qtophmeo  23809  fbdmn0  23826  fbasrn  23876  elfm3  23942  fmfnfmlem4  23949  fclscf  24017  cnpfcf  24033  alexsubALTlem3  24041  tsmsres  24136  blval2  24559  tnggrpr  24660  nmoleub  24736  nmhmcn  25135  ncvs1  25173  iscau4  25295  caussi  25313  cmssmscld  25366  cmslssbn  25388  cniccbdd  25478  ovoliunnul  25524  mbfinf  25682  itg2splitlem  25766  dvcn  25939  c1lip1  26018  c1lip3  26020  dvcnvrelem1  26038  dvfsumlem2  26049  ply1divex  26161  quotcan  26334  aannenlem1  26353  taylf  26385  taylthlem2  26399  ulmcaulem  26420  ulmcau  26421  reeff1o  26474  logccv  26687  rtprmirr  26785  logreclem  26787  isosctrlem2  26844  xrlimcnp  26993  rlimcxp  26999  ftalem7  27104  vmappw  27141  fsumdvdsmul  27220  fsumvma  27239  dchreq  27284  dchrptlem1  27290  dchrsum  27295  bposlem7  27316  lgsqrlem2  27373  lgsdchr  27381  gausslemma2dlem1a  27391  lgseisenlem2  27402  lgsquad2  27412  2lgslem1b  27418  2sqlem6  27449  2sqnn0  27464  addsq2reu  27466  2sqreulem2  27478  sltval2  27683  sltres  27689  nodenselem8  27718  nodense  27719  noresle  27724  scutun12  27837  madeval2  27874  elmade  27888  negsf1o  28060  muls0ord  28183  recsex  28215  noseqrdgfn  28277  n0subs  28323  tgcgrcomimp  28401  isperp2  28639  xmstrkgc  28816  brbtwn  28830  brcgr  28831  axcgrid  28847  axeuclidlem  28893  axeuclid  28894  elntg2  28916  lpvtx  29001  upgrex  29025  upgrpredgv  29072  upgredgpr  29075  uhgr0v0e  29171  subgrprop  29206  fusgrfisbase  29261  edgnbusgreu  29300  nbusgredgeu0  29301  cusgredg  29357  structtocusgr  29379  cusgrsize2inds  29387  cusgrsize  29388  usgredgsscusgredg  29393  fusgrmaxsize  29398  uspgrloopvtxel  29450  umgr2v2e  29459  vtxdginducedm1fi  29478  finsumvtxdg2sstep  29483  rgrprop  29494  rusgrprop  29496  0uhgrrusgr  29512  rusgrpropedg  29518  ewlkprop  29537  upgrewlkle2  29540  wlkprop  29545  upgrwlkcompim  29577  uspgr2wlkeq  29580  wlklenvclwlk  29589  wlkonprop  29592  wlkres  29604  redwlk  29606  wlkdlem2  29617  wksonproplem  29638  wksonproplemOLD  29639  usgr2trlspth  29695  usgr2pth  29698  pthdlem1  29700  crctcshwlkn0lem4  29744  wwlksnprcl  29770  wlkiswwlks2  29806  wwlksm1edg  29812  wlknewwlksn  29818  wwlksnred  29823  wwlksnextbi  29825  wwlksnextwrd  29828  wwlksnextinj  29830  wwlksnextsurj  29831  umgr2wlk  29880  umgrwwlks2on  29888  elwwlks2  29897  clwwlk1loop  29918  umgrclwwlkge2  29921  clwlkclwwlklem2a1  29922  clwlkclwwlklem2a4  29927  clwlkclwwlklem2a  29928  clwlkclwwlklem2  29930  clwlkclwwlkfo  29939  clwwisshclwwslemlem  29943  clwwlknwwlksn  29968  clwwlknlbonbgr1  29969  clwwlkn1loopb  29973  clwwlkf  29977  clwwlknon1  30027  clwwlknonwwlknonb  30036  clwwlknonex2lem2  30038  vdn0conngrumgrv2  30126  frgrnbnb  30223  frgrncvvdeqlem2  30230  frgrncvvdeqlem3  30231  frgrncvvdeqlem6  30234  frgrwopreglem4a  30240  fusgr2wsp2nb  30264  frrusgrord0lem  30269  numclwwlk2lem1lem  30272  2clwwlk2clwwlklem  30276  2clwwlk2clwwlk  30280  numclwwlk1lem2foa  30284  numclwwlk1lem2f1  30287  frgrreg  30324  hlipgt0  30844  ocin  31226  ocnel  31228  shmodsi  31319  pjmf1  31646  unopf1o  31846  staddi  32176  stadd3i  32178  mdi  32225  dmdmd  32230  dmdi  32232  dmdbr2  32233  dmdbr3  32235  dmdbr4  32236  dmdi4  32237  mdsl1i  32251  superpos  32284  cvbr4i  32297  atssma  32308  atcv1  32310  atomli  32312  chirredlem1  32320  addltmulALT  32376  bian1dOLD  32383  ifeqeqx  32463  disjxpin  32508  suppss3  32638  fpwrelmap  32647  expgt0b  32720  ogrpaddlt  32956  qsfld  33379  ply1degltdimlem  33523  ply1degltdim  33524  metider  33722  tpr2rico  33740  xrge0iifiso  33763  qqhcn  33819  qqhucn  33820  esumlub  33906  esumpinfval  33919  esumpinfsum  33923  ballotlemfc0  34339  ballotlemfcc  34340  ftc2re  34457  bnj517  34743  fnrelpredd  34939  pfxwlk  34964  subgrwlk  34973  loop1cycl  34978  erdsze2lem2  35045  satfv1  35204  satfdmlem  35209  satf0op  35218  fmlasuc  35227  dfrdg4  35788  altopthsn  35798  btwncomim  35850  btwnexch3  35857  btwnexch2  35860  endofsegid  35922  opnrebl2  36046  nn0prpwlem  36047  onsuct0  36166  ordcmp  36172  nndivsub  36182  dnibndlem13  36206  bj-cbval  36366  bj-cbvex  36367  bj-cbvexw  36393  bj-cbv3tb  36505  bj-spimtv  36512  bj-equsal  36544  bj-sbsb  36555  bj-vtoclf  36634  bj-zfauscl  36643  bj-gabss  36654  bj-gabeqd  36656  currysetlem2  36668  bj-snsetex  36683  bj-ismooredr2  36830  bj-inftyexpiinj  36929  bj-finsumval0  37005  bj-fvimacnv0  37006  bj-bary1lem1  37031  bj-bary1  37032  f1omptsnlem  37056  iooelexlt  37082  relowlpssretop  37084  rdgeqoa  37090  finxpsuclem  37117  fvineqsneq  37132  pibt2  37137  wl-equsal1i  37252  wl-ax11-lem10  37302  ltflcei  37322  sin2h  37324  cos2h  37325  tan2h  37326  lindsenlbs  37329  matunitlindf  37332  poimirlem3  37337  poimirlem4  37338  poimirlem18  37352  poimirlem20  37354  poimirlem21  37355  poimirlem22  37356  poimirlem24  37358  poimirlem25  37359  poimirlem26  37360  poimirlem27  37361  poimirlem28  37362  poimirlem31  37365  poimir  37367  heicant  37369  mblfinlem1  37371  mblfinlem2  37372  mblfinlem3  37373  mblfinlem4  37374  mbfresfi  37380  cnambfre  37382  ftc1anc  37415  dvasin  37418  areacirclem1  37422  areacirclem4  37425  areacirc  37427  brabg2  37431  fzmul  37455  fdc  37459  incsequz2  37463  isbnd2  37497  opidonOLD  37566  opidon2OLD  37568  grpomndo  37589  elghomlem2OLD  37600  rngoueqz  37654  dvrunz  37668  divrngidl  37742  refressn  38154  dral1-o  38615  lsatn0  38710  l1cvpat  38765  leat2  39005  atnle  39028  cvlcvr1  39050  cvrexchlem  39131  cvratlem  39133  cvrat  39134  atcvrj0  39140  atle  39148  snatpsubN  39462  linepsubN  39464  pmapsub  39480  lneq2at  39490  lncvrelatN  39493  2llnma3r  39500  cdlemblem  39505  paddasslem5  39536  poml4N  39665  lhpmcvr4N  39738  trlval2  39875  cdlemd6  39915  cdleme7ga  39960  cdleme25b  40066  cdleme29b  40087  cdleme35fnpq  40161  cdleme50f1  40255  cdlemf1  40273  cdlemg27b  40408  cdlemk28-3  40620  tendospcanN  40735  diaf11N  40761  dia2dimlem1  40776  dibf11N  40873  dihf11  40979  dihmeetlem1N  41002  dochvalr  41069  dochnel2  41104  dvh4dimlem  41155  dochsat0  41169  mapd1o  41360  hdmapf1oN  41577  hgmapval0  41604  hgmapf1oN  41615  hlhilhillem  41676  nnproddivdvdsd  41712  lcmineqlem  41764  aks4d1p1p5  41787  aks4d1p3  41790  aks4d1p8d2  41797  aks4d1p8  41799  aks4d1p9  41800  fldhmf1  41802  isprimroot2  41806  primrootsunit1  41809  primrootscoprmpow  41811  posbezout  41812  primrootscoprbij  41814  primrootlekpowne0  41817  primrootspoweq0  41818  aks6d1c1p1  41819  aks6d1c1p2  41821  aks6d1c1p3  41822  aks6d1c1p4  41823  aks6d1c1p5  41824  aks6d1c1p7  41825  aks6d1c1p6  41826  aks6d1c1p8  41827  aks6d1c2p2  41831  aks6d1c2lem3  41838  aks6d1c2lem4  41839  hashnexinj  41840  hashnexinjle  41841  aks6d1c2  41842  aks6d1c5lem0  41847  aks6d1c5lem1  41848  aks6d1c5  41851  sticksstones1  41858  sticksstones3  41860  sticksstones8  41865  sticksstones11  41868  sticksstones12  41870  sticksstones20  41878  sticksstones22  41880  aks6d1c6lem3  41884  aks6d1c6lem4  41885  aks6d1c6isolem1  41886  aks6d1c6isolem2  41887  aks6d1c6lem5  41889  aks6d1c7  41896  rhmqusspan  41897  unitscyglem2  41908  unitscyglem3  41909  metakunt7  41919  sn-axprlem3  41961  oexpreposd  42048  frlmsnic  42230  fsuppind  42280  prjspval  42293  rexrabdioph  42488  fphpdo  42511  irrapxlem3  42518  rmxypairf1o  42606  rmxycomplete  42612  zindbi  42641  lermxnn0  42645  ltrmy  42647  rmyeq0  42648  rmyeq  42649  lermy  42650  acongsym  42671  acongneg2  42672  wepwsolem  42740  onsupuni  42931  onsupmaxb  42941  onsucf1o  42975  onov0suclim  42977  oe0suclim  42980  onsucwordi  42991  cantnfresb  43027  omabs2  43035  tfsconcat0b  43049  tfsconcatrev  43051  naddcnffo  43067  oaun3lem1  43077  oaltom  43109  omltoe  43111  sdomne0  43117  sdomne0d  43118  safesnsupfidom1o  43121  intabssd  43223  iscard4  43237  ss2iundf  43363  frege129d  43467  frege133d  43469  axfrege52a  43560  axfrege52c  43591  ntrk0kbimka  43743  gneispace  43838  suprleubrd  43870  suprlubrd  43872  radcnvrat  44025  nzss  44028  expgrowthi  44044  ordpss  44162  bi23impib  44198  bi23imp13  44204  rspsbc2  44247  tratrb  44249  sbcim2g  44251  truniALT  44254  3impcombi  44530  tpid3gVD  44555  orbi1rVD  44561  sbc3orgVD  44564  rspsbc2VD  44568  tratrbVD  44574  sbcim2gVD  44588  sbcbiVD  44589  truniALTVD  44591  trintALTVD  44593  trintALT  44594  csbingVD  44597  csbsngVD  44606  csbxpgVD  44607  csbresgVD  44608  csbrngVD  44609  csbima12gALTVD  44610  csbunigVD  44611  csbfv12gALTVD  44612  relopabVD  44614  isosctrlem1ALT  44647  fzisoeu  44951  xrralrecnnge  45041  allbutfi  45044  climinf  45263  liminfreuzlem  45459  climliminf  45463  climliminflimsup  45465  xlimpnfxnegmnf  45471  xlimbr  45484  stoweidlem7  45664  stoweidlem62  45719  sge0gerpmpt  46059  meaiuninclem  46137  carageniuncllem2  46179  issmflem  46384  et-sqrtnegnre  46530  natlocalincr  46531  tworepnotupword  46541  funressnfv  46694  funressnvmo  46696  f1cof1b  46726  2reu3  46759  ralbinrald  46771  afv0fv0  46798  afv0nbfvbi  46800  afvfv0bi  46801  fnbrafvb  46803  afvres  46821  tz6.12-afv  46822  afvco2  46825  ndmaovcl  46852  afv2res  46888  tz6.12-afv2  46889  nelbrim  46924  f1oresf1o2  46940  zm1nn  46951  nltle2tri  46962  subsubelfzo0  46975  iccpartres  47026  iccpartiltu  47030  fargshiftfv  47047  ichnreuop  47080  ichreuopeq  47081  prsprel  47095  sprsymrelf1lem  47099  sprsymrelfolem2  47101  sprsymrelfo  47105  prpair  47109  paireqne  47119  sbcpr  47129  fmtnof1  47143  goldbachthlem2  47154  fmtnoprmfac1  47173  fmtnoprmfac2  47175  lighneallem2  47214  lighneallem4b  47217  lighneallem4  47218  evennodd  47251  oddneven  47252  oexpnegnz  47286  evenltle  47325  fpprwppr  47347  fpprwpprb  47348  gbowge7  47371  gbege6  47373  sbgoldbwt  47385  sbgoldbst  47386  nnsum3primesle9  47402  bgoldbtbndlem2  47414  grimprop  47484  isuspgrimlem  47489  uhgrimisgrgriclem  47513  clnbgrgrimlem  47516  grlimprop  47526  clintop  47621  isassintop  47623  lidldomn1  47644  uzlidlring  47648  2zrngnmlid2  47670  rngccatidALTV  47685  ringccatidALTV  47719  srhmsubcALTV  47738  ztprmneprm  47762  pgrpgt2nabl  47781  lindslinindimp2lem4  47880  lincresunit3  47900  fldivexpfllog2  47989  digexp  48031  naryfvalelfv  48056  affinecomb1  48126  eenglngeehlnmlem1  48161  eenglngeehlnmlem2  48162  eenglngeehlnm  48163  itscnhlc0yqe  48183  itsclc0yqsol  48188  itscnhlc0xyqsol  48189  itschlc0xyqsol1  48190  itschlc0xyqsol  48191  itsclquadeu  48201  inlinecirc02plem  48210  inlinecirc02p  48211  pm4.71da  48213  mofsn  48247  seposep  48295  idmon  48373  idepi  48374  prsthinc  48411  grptcmon  48453  grptcepi  48454  spd  48460  spcdvw  48461  setrec2fun  48474