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 ⊢ (𝜑 → (𝜒 → 𝜓))

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:  biimtrrdi  257  mpbird  260  sylibrd  262  sylbird  263  con4bid  320  mtbid  327  mtbii  329  imbi1d  344  biimpar  482  prlem1  1068  alexbii  1860  speivw  2000  spfw  2060  cbvalw  2062  alcomimw  2070  cbvalv1  2379  cbval  2436  axc16i  2474  sb3  2515  sb2  2517  axc16gALT  2528  ralbida  3282  rspcimdv  3580  rspcedv  3583  moi2  3688  moi  3690  sspsstr  4071  2nreu  4415  rabsnifsb  4693  ralxfr2d  5384  axprlem4OLD  5404  sbcop1  5473  isso2i  5609  wefrc  5658  elinxp  6021  sotri3  6133  oneqmini  6417  ordsssuc2  6457  ordtri2or  6464  iotan0  6529  2elresin  6659  f1ocnv  6836  fveqres  6928  fvun1  6975  dffo4  7101  funopsnOLD  7148  fconst5  7207  fnprb  7209  fntpb  7210  isores3  7336  f1owe  7354  weniso  7355  ndmovordi  7604  abnexg  7757  ordsuc  7812  orduniorsuc  7828  ordzsl  7843  tfinds  7858  dmfexALT  7907  f1oweALT  7971  opreuopreu  8033  fnse  8131  poxp3  8148  poseq  8156  soseq  8157  tposfo2  8247  fprlem1  8299  issmo2  8338  iordsmo  8346  smoel2  8352  tz7.48lem  8430  oawordeulem  8541  om00  8562  omlimcl  8565  odi  8566  nnawordi  8609  unfi  9157  php2  9194  fiint  9288  fipreima  9317  dffi2  9385  suplub2  9423  wemapsolem  9514  unwdomg  9548  inf3lem3  9601  trcl  9699  frrlem15  9731  fidomtri  9981  prdom2  9992  cardaleph  10075  ackbij1lem16  10219  coflim  10247  coftr  10259  infpssrlem4  10292  isfin7-2  10382  axdc3lem2  10437  axdc3lem4  10439  brdom6disj  10518  entric  10543  fpwwe2lem11  10628  inatsk  10765  grur1a  10806  indpi  10894  reclem3pr  11036  supsrlem  11098  lelttr  11302  dedekindle  11376  negn0  11645  fimaxre  12161  fiminre  12164  nnmulcl  12259  arch  12503  nnnegz  12596  zle0orge1  12610  zeo  12684  uzm1  12898  rpneg  13052  xrlttri  13166  xrlelttr  13183  iccid  13419  icoshft  13502  fzen  13571  elfz1b  13623  fzdif1  13635  elfz2nn0  13648  fzoopth  13793  fleqceilz  13889  zmodidfzoimp  13936  modsumfzodifsn  13982  hasheqf1oi  14389  hashnfinnn0  14399  hashle2prv  14517  swrd0  14698  pfxccatin12lem2  14770  swrdccat  14774  swrdccat3blem  14778  repswswrd  14823  trclublem  15034  max0add  15363  abslt  15368  absle  15369  rexuzre  15406  caurcvg  15730  caucvg  15732  dvdsval2  16315  negdvdsb  16332  muldvds2  16341  dvdsabseq  16373  smuval2  16542  smupvallem  16543  rplpwr  16618  alginv  16635  algfx  16640  coprmgcdb  16709  divgcdcoprm0  16725  oddprmgt2  16760  rpexp1i  16784  qnumdencl  16800  phiprmpw  16837  prmdiveq  16847  prm23lt5  16876  pcmpt  16954  infpnlem1  16972  prmgaplem3  17115  prmgaplem8  17120  imasaddfnlem  17584  plelttr  18400  lubval  18412  lublecllem  18416  glbval  18425  mndind  18889  mndodconglem  19613  sdrgacs  20884  xrge0omnd  21566  elfrlmbasn0  21884  mavmulsolcl  22679  slesolex  22810  fvmptnn04if  22977  chfacfisf  22982  chfacfisfcpmat  22983  cnpnei  23392  unconn  23557  comppfsc  23660  kqsat  23859  isr0  23865  qtophmeo  23945  trufil  24038  alexsubALT  24179  cnextcn  24195  ucnima  24408  iducn  24410  bl2in  24528  addcnlem  24993  rescncf  25027  ovoliunlem2  25633  voliun  25684  mbflimsup  25796  itgcn  25975  dvdsq1p  26291  aalioulem2  26465  recosf1o  26668  logrec  26896  xrlimcnp  27101  basellem4  27216  bposlem1  27416  bposlem5  27420  lgsqrmod  27484  lgsdchrval  27486  2lgslem1a1  27521  pntlem3  27741  nosupbnd1  27846  noinfbnd1  27861  oldbday  28062  lrcut  28065  abslts  28410  n0ssoldg  28514  zsoring  28570  bdayfinbndlem1  28628  isplng  29020  brbtwn2  29198  axbtwnid  29232  elntg2  29278  umgredgprv  29400  umgrpredgv  29433  usgredgprvALT  29488  fusgrfisstep  29622  fusgrfis  29623  nbupgr  29637  nbumgrvtx  29639  finsumvtxdg2size  29843  wlkp1lem8  29971  upgr2pthnlp  30024  wwlksnextinj  30191  usgr2wspthons3  30259  clwwlkccatlem  30283  clwlkclwwlklem2a1  30286  clwwisshclwws  30309  wwlksext2clwwlk  30351  clwwlknonex2lem2  30402  eucrctshift  30537  eucrct2eupth  30539  numclwwlk2lem1  30670  numclwwlk5lem  30681  frgrreggt1  30687  frgrreg  30688  friendship  30693  blocn2  31103  htthlem  31212  axhcompl-zf  31293  spanuni  31839  spansncol  31863  spansneleq  31865  elspansn5  31869  idcnop  32276  pjnormssi  32463  dmdmd  32595  n0nsnel  32804  ifeqeqx  32831  opabssi  32901  ac6mapd  32911  ressupprn  32978  supxrnemnf  33056  rexdiv  33188  xrstos  33273  cnre2csqlem  34247  fsumcvg4  34287  lmxrge0  34289  qqhval2lem  34318  esumpr2  34404  esumcvg  34423  issgon  34460  measxun2  34547  measres  34559  measdivcst  34561  measdivcstALTV  34562  elorrvc  34801  signsply0  34885  bnj580  35248  nummin  35429  axprALT2  35448  kardfi  35518  0nn0m1nnn0  35539  umgracycusgr  35581  erdsze2lem2  35631  cvmsval  35693  fmlasuc  35813  fundmpss  36194  dfon2lem3  36210  dfrdg4  36378  cgrtriv  36429  btwntriv2  36439  ifscgr  36471  lineext  36503  btwnconn1lem12  36525  colinbtwnle  36545  elicc3  36753  ontgval  36867  onsucconni  36873  axtco1from2  36911  axtcond  36914  axnulregtco  36916  dfttc4lem2  36965  bj-bibibi  37104  bj-cbvalvv  37186  bj-cbval  37193  bj-cbvex  37194  bj-cbvexw  37224  bj-nnf-cbval  37330  bj-equsal  37386  bj-gabeqd  37498  bj-restn0  37657  bj-snmoore  37680  cgsex2gd  37706  bj-elsn0  37724  bj-finsumval0  37854  relowlssretop  37934  sucneqond  37936  finxpsuc  37969  pibt2  37988  wl-nfs1t  38117  finixpnum  38181  ltflcei  38184  matunitlindflem1  38192  poimirlem23  38219  poimirlem24  38220  poimirlem27  38223  poimirlem32  38228  itg2addnclem  38247  areacirclem2  38285  areacirclem5  38288  areacirc  38289  nninfnub  38327  prdstotbnd  38370  heiborlem4  38390  heibor  38397  elghomlem2OLD  38462  grpokerinj  38469  isidlc  38591  disjlem17  39478  prtlem17  39577  dral1-o  39605  axc16g-o  39635  lsator0sp  39702  atlrelat1  40022  cvratlem  40122  diaintclN  41759  dibintclN  41868  cdlemn11pre  41911  dihord2pre  41926  dihintcl  42045  dochkrshp4  42090  lcfrlem9  42251  lcfrlem21  42264  mapdh8e  42485  aks4d1p5  42774  aks6d1c1p1  42801  sticksstones4  42843  0prjspnrel  43288  elrfirn2  43356  rencldnfilem  43476  onsupnmax  43884  onov0suclim  43930  oege1  43962  cantnfresb  43980  dflim5  43985  omabs2  43988  refimssco  44262  rtrclex  44272  intimasn  44312  ss2iundf  44314  ov2ssiunov2  44355  comptiunov2i  44361  iunrelexpuztr  44374  dssmapf1od  44676  mnringmulrcld  44881  mnuprdlem1  44911  mnuprdlem2  44912  snelpwrVD  45468  en3lplem1VD  45480  en3lpVD  45482  orbi1rVD  45485  sbc3orgVD  45488  3impexpVD  45493  equncomVD  45505  trsbcVD  45514  trintALTVD  45517  trintALT  45518  csbingVD  45521  csbsngVD  45530  csbxpgVD  45531  csbrngVD  45533  csbfv12gALTVD  45536  relopabVD  45538  e2ebindVD  45549  xlimpnfxnegmnf  46457  xlimbr  46470  stoweidlem35  46678  stoweidlem48  46691  ormkglobd  47520  cjnpoly  47552  tannpoly  47553  n0nsn2el  47688  rexrsb  47763  2reu8i  47776  funbrafv  47821  rlimdmafv  47840  tz6.12c-afv2  47905  rlimdmafv2  47921  fzopredsuc  47987  2ffzoeq  47991  m1modnep2mod  48021  2timesltsq  48041  eqfvelsetpreimafv  48068  iccpartlt  48099  proththd  48292  even3prm2  48410  fppr2odd  48422  sbgoldbm  48475  nnsum3primesle9  48485  wtgoldbnnsum4prm  48493  bgoldbnnsum3prm  48495  grtrif1o  48633  mgm2mgm  48918  2zrngnmlid  48946  2zrngnmrid  48947  ellcoellss  49137  nneop  49228  fldivexpfllog2  49267  digexp  49309  reorelicc  49412  2itscp  49483  oppc1stflem  49987  prsthinc  50164  elpglem2  50412