Theorem biimprd 251

Description: Deduce a converse implication from a logical equivalence. Deduction associated with biimpr 223 and biimpri 231. (Contributed by NM, 11-Jan-1993.) (Proof shortened by Wolf Lammen, 22-Sep-2013.)

Hypothesis

Ref	Expression
biimprd.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
biimprd	⊢ (𝜑 → (𝜒 → 𝜓))

Proof of Theorem biimprd

Step	Hyp	Ref	Expression
1		id 23	. 2 ⊢ (𝜒 → 𝜒)
2		biimprd.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	imbitrrid 249	1 ⊢ (𝜑 → (𝜒 → 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  biimtrrdi  257  mpbird  260  sylibrd  262  sylbird  263  con4bid  320  mtbid  327  mtbii  329  imbi1d  344  biimpar  483  prlem1  1070  alexbii  1866  speivw  2006  spfw  2066  cbvalw  2068  alcomimw  2076  cbvalv1  2370  cbval  2427  axc16i  2465  sb3  2506  sb2  2508  axc16gALT  2519  ralbida  3273  rspcimdv  3566  rspcedv  3569  moi2  3674  moi  3676  sspsstr  4057  2nreu  4402  rabsnifsb  4683  ralxfr2d  5375  axprlem4OLD  5395  sbcop1  5464  isso2i  5600  wefrc  5649  elinxp  6014  sotri3  6126  oneqmini  6413  ordsssuc2  6453  ordtri2or  6460  iotan0  6525  2elresin  6656  f1ocnv  6833  fveqres  6925  fvun1  6972  dffo4  7099  funopsnOLD  7148  fconst5  7208  fnprb  7210  fntpb  7211  isores3  7339  f1oweOLD  7358  weniso  7360  ndmovordi  7608  abnexg  7761  ordsuc  7816  orduniorsuc  7832  ordzsl  7847  tfinds  7862  dmfexALT  7911  f1oweALT  7975  opreuopreu  8037  fnse  8136  poxp3  8153  poseq  8161  soseq  8162  tposfo2  8252  fprlem1  8304  issmo2  8343  iordsmo  8351  smoel2  8357  tz7.48lemOLD  8437  oawordeulem  8548  om00  8569  omlimcl  8572  odi  8573  nnawordi  8616  unfi  9172  php2  9209  fiint  9303  fipreima  9332  dffi2  9400  suplub2  9438  wemapsolem  9529  unwdomg  9563  inf3lem3  9616  wemapwe  9683  trcl  9714  frrlem15  9746  fidomtri  10023  prdom2  10034  cardaleph  10117  ackbij1lem16  10261  coflim  10288  coftr  10300  infpssrlem4  10333  isfin7-2  10423  axdc3lem2  10478  axdc3lem4  10480  brdom6disj  10560  entric  10590  fpwwe2lem11  10675  inatsk  10812  grur1a  10853  indpi  10941  reclem3pr  11083  supsrlem  11145  lelttr  11349  dedekindle  11423  negn0  11692  fimaxre  12208  fiminre  12211  nnmulcl  12306  arch  12550  nnnegz  12643  zle0orge1  12657  0nn0m1nnn0  12700  zeo  12732  uzm1  12946  rpneg  13101  xrlttri  13215  xrlelttr  13232  iccid  13468  icoshft  13551  fzen  13620  elfz1b  13673  fzdif1  13685  elfz2nn0  13698  fzoopth  13843  fleqceilz  13940  zmodidfzoimp  13987  modsumfzodifsn  14033  hasheqf1oi  14440  hashnfinnn0  14450  hashle2prv  14568  swrd0  14753  pfxccatin12lem2  14825  swrdccat  14829  swrdccat3blem  14833  repswswrd  14880  trclublem  15093  max0add  15422  abslt  15427  absle  15428  rexuzre  15465  caurcvg  15789  caucvg  15791  dvdsval2  16370  negdvdsb  16387  muldvds2  16396  dvdsabseq  16428  smuval2  16597  smupvallem  16598  rplpwr  16673  alginv  16690  algfx  16695  coprmgcdb  16764  divgcdcoprm0  16780  oddprmgt2  16815  rpexp1i  16839  qnumdencl  16855  phiprmpw  16892  prmdiveq  16902  prm23lt5  16931  pcmpt  17009  infpnlem1  17027  prmgaplem3  17170  prmgaplem8  17175  imasaddfnlem  17639  plelttr  18455  lubval  18467  lublecllem  18471  glbval  18480  mndind  18963  mndodconglem  19694  sdrgacs  20997  xrge0omnd  21690  elfrlmbasn0  22008  mavmulsolcl  22805  matunitlindflem1  22933  slesolex  22939  fvmptnn04if  23106  chfacfisf  23111  chfacfisfcpmat  23112  cnpnei  23521  unconn  23686  comppfsc  23790  kqsat  23989  isr0  23995  qtophmeo  24075  trufil  24168  alexsubALT  24309  cnextcn  24325  ucnima  24538  iducn  24540  bl2in  24658  addcnlem  25123  rescncf  25157  ovoliunlem2  25763  voliun  25814  mbflimsup  25926  itgcn  26104  dvdsq1p  26420  preimaaa  26587  aalioulem2  26601  recosf1o  26804  logrec  27032  xrlimcnp  27237  basellem4  27352  bposlem1  27552  bposlem5  27556  lgsqrmod  27620  lgsdchrval  27622  2lgslem1a1  27657  pntlem3  27877  nosupbnd1  27982  noinfbnd1  27997  oldbday  28198  lrcut  28201  abslts  28546  n0ssoldg  28650  zsoring  28706  bdayfinbndlem1  28764  isplng  29167  brbtwn2  29394  axbtwnid  29428  elntg2  29474  umgredgprv  29596  umgrpredgv  29629  usgredgprvALT  29687  fusgrfisstep  29821  fusgrfis  29822  nbupgr  29836  nbumgrvtx  29838  finsumvtxdg2size  30042  wlkp1lem8  30170  upgr2pthnlp  30229  wwlksnextinj  30399  usgr2wspthons3  30467  clwwlkccatlem  30491  clwlkclwwlklem2a1  30494  clwwisshclwws  30517  wwlksext2clwwlk  30559  clwwlknonex2lem2  30610  eucrctshift  30755  eucrct2eupth  30757  numclwwlk2lem1  30888  numclwwlk5lem  30899  frgrreggt1  30905  frgrreg  30906  friendship  30911  blocn2  31321  htthlem  31430  axhcompl-zf  31511  spanuni  32057  spansncol  32081  spansneleq  32083  elspansn5  32087  idcnop  32494  pjnormssi  32681  dmdmd  32813  n0nsnel  33022  ifeqeqx  33049  opabssi  33118  ac6mapd  33128  ressupprn  33194  supxrnemnf  33271  rexdiv  33403  xrstos  33482  cnre2csqlem  34453  fsumcvg4  34493  lmxrge0  34495  qqhval2lem  34524  esumpr2  34610  esumcvg  34629  issgon  34666  measxun2  34754  measres  34766  measdivcst  34768  measdivcstALTV  34769  elorrvc  35008  signsply0  35092  bnj580  35455  fnfvintima  35624  nummin  35631  axprALT2  35650  kardfi  35739  umgracycusgr  35816  erdsze2lem2  35866  cvmsval  35928  fmlasuc  36048  fundmpss  36429  dfon2lem3  36445  dfrdg4  36613  cgrtriv  36665  btwntriv2  36675  ifscgr  36707  lineext  36739  btwnconn1lem12  36761  colinbtwnle  36781  elicc3  37003  ontgval  37117  onsucconni  37123  axtco1from2  37161  axtcond  37164  axnulregtco  37166  dfttc4lem2  37215  bj-bibibi  37354  bj-cbvalvv  37436  bj-cbval  37443  bj-cbvex  37444  bj-cbvexw  37474  bj-nnf-cbval  37580  bj-equsal  37636  bj-gabeqd  37748  bj-restn0  37907  bj-snmoore  37930  cgsex2gd  37954  bj-elsn0  37972  bj-finsumval0  38102  relowlssretop  38182  sucneqond  38184  finxpsuc  38217  pibt2  38236  wl-nfs1t  38365  finixpnum  38424  ltflcei  38427  poimirlem23  38457  poimirlem24  38458  poimirlem27  38461  poimirlem32  38466  itg2addnclem  38485  areacirclem2  38523  areacirclem5  38526  areacirc  38527  nninfnub  38566  prdstotbnd  38609  heiborlem4  38629  heibor  38636  elghomlem2OLD  38701  grpokerinj  38708  isidlc  38830  disjlem17  39715  prtlem17  39814  dral1-o  39842  axc16g-o  39872  lsator0sp  39939  atlrelat1  40259  cvratlem  40359  diaintclN  41996  dibintclN  42105  cdlemn11pre  42148  dihord2pre  42163  dihintcl  42282  dochkrshp4  42327  lcfrlem9  42488  lcfrlem21  42501  mapdh8e  42722  aks4d1p5  43011  aks6d1c1p1  43038  sticksstones4  43080  0prjspnrel  43538  elrfirn2  43606  rencldnfilem  43726  onsupnmax  44134  onov0suclim  44180  oege1  44212  cantnfresb  44230  dflim5  44235  omabs2  44238  refimssco  44512  rtrclex  44522  intimasn  44562  ss2iundf  44564  ov2ssiunov2  44605  comptiunov2i  44611  iunrelexpuztr  44624  dssmapf1od  44926  mnringmulrcld  45131  mnuprdlem1  45161  mnuprdlem2  45162  snelpwrVD  45718  en3lplem1VD  45730  en3lpVD  45732  orbi1rVD  45735  sbc3orgVD  45738  3impexpVD  45743  equncomVD  45755  trsbcVD  45764  trintALTVD  45767  trintALT  45768  csbingVD  45771  csbsngVD  45780  csbxpgVD  45781  csbrngVD  45783  csbfv12gALTVD  45786  relopabVD  45788  e2ebindVD  45799  xlimpnfxnegmnf  46707  xlimbr  46720  stoweidlem35  46928  stoweidlem48  46941  ormkglobd  47770  n0nsn2el  47978  rexrsb  48053  2reu8i  48066  funbrafv  48111  rlimdmafv  48130  tz6.12c-afv2  48195  rlimdmafv2  48211  fzopredsuc  48277  2ffzoeq  48281  m1modnep2mod  48311  2timesltsq  48331  eqfvelsetpreimafv  48358  iccpartlt  48389  proththd  48582  even3prm2  48700  fppr2odd  48712  sbgoldbm  48765  nnsum3primesle9  48775  wtgoldbnnsum4prm  48783  bgoldbnnsum3prm  48785  grtrif1o  48923  mgm2mgm  49207  2zrngnmlid  49235  2zrngnmrid  49236  ellcoellss  49430  nneop  49521  fldivexpfllog2  49560  digexp  49602  reorelicc  49705  2itscp  49776  oppc1stflem  50278  prsthinc  50455  elpglem2  50703