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  482  prlem1  1070  alexbii  1863  speivw  2003  spfw  2063  cbvalw  2065  alcomimw  2073  cbvalv1  2373  cbval  2430  axc16i  2468  sb3  2509  sb2  2511  axc16gALT  2522  ralbida  3276  rspcimdv  3571  rspcedv  3574  moi2  3679  moi  3681  sspsstr  4063  2nreu  4409  rabsnifsb  4688  ralxfr2d  5381  axprlem4OLD  5401  sbcop1  5470  isso2i  5606  wefrc  5655  elinxp  6018  sotri3  6130  oneqmini  6414  ordsssuc2  6454  ordtri2or  6461  iotan0  6526  2elresin  6656  f1ocnv  6833  fveqres  6925  fvun1  6972  dffo4  7098  funopsnOLD  7145  fconst5  7204  fnprb  7206  fntpb  7207  isores3  7333  f1owe  7351  weniso  7352  ndmovordi  7601  abnexg  7751  ordsuc  7806  orduniorsuc  7822  ordzsl  7837  tfinds  7852  dmfexALT  7901  f1oweALT  7965  opreuopreu  8027  fnse  8125  poxp3  8142  poseq  8150  soseq  8151  tposfo2  8241  fprlem1  8293  issmo2  8332  iordsmo  8340  smoel2  8346  tz7.48lem  8424  oawordeulem  8535  om00  8556  omlimcl  8559  odi  8560  nnawordi  8603  unfi  9151  php2  9188  fiint  9282  fipreima  9311  dffi2  9379  suplub2  9417  wemapsolem  9508  unwdomg  9542  inf3lem3  9595  trcl  9693  frrlem15  9725  fidomtri  9984  prdom2  9995  cardaleph  10078  ackbij1lem16  10222  coflim  10249  coftr  10261  infpssrlem4  10294  isfin7-2  10384  axdc3lem2  10439  axdc3lem4  10441  brdom6disj  10520  entric  10545  fpwwe2lem11  10630  inatsk  10767  grur1a  10808  indpi  10896  reclem3pr  11038  supsrlem  11100  lelttr  11304  dedekindle  11378  negn0  11647  fimaxre  12163  fiminre  12166  nnmulcl  12261  arch  12505  nnnegz  12598  zle0orge1  12612  zeo  12686  uzm1  12900  rpneg  13054  xrlttri  13168  xrlelttr  13185  iccid  13421  icoshft  13504  fzen  13573  elfz1b  13626  fzdif1  13638  elfz2nn0  13651  fzoopth  13796  fleqceilz  13892  zmodidfzoimp  13939  modsumfzodifsn  13985  hasheqf1oi  14392  hashnfinnn0  14402  hashle2prv  14520  swrd0  14701  pfxccatin12lem2  14773  swrdccat  14777  swrdccat3blem  14781  repswswrd  14826  trclublem  15037  max0add  15366  abslt  15371  absle  15372  rexuzre  15409  caurcvg  15733  caucvg  15735  dvdsval2  16317  negdvdsb  16334  muldvds2  16343  dvdsabseq  16375  smuval2  16544  smupvallem  16545  rplpwr  16620  alginv  16637  algfx  16642  coprmgcdb  16711  divgcdcoprm0  16727  oddprmgt2  16762  rpexp1i  16786  qnumdencl  16802  phiprmpw  16839  prmdiveq  16849  prm23lt5  16878  pcmpt  16956  infpnlem1  16974  prmgaplem3  17117  prmgaplem8  17122  imasaddfnlem  17586  plelttr  18402  lubval  18414  lublecllem  18418  glbval  18427  mndind  18891  mndodconglem  19615  sdrgacs  20913  xrge0omnd  21604  elfrlmbasn0  21922  mavmulsolcl  22717  slesolex  22848  fvmptnn04if  23015  chfacfisf  23020  chfacfisfcpmat  23021  cnpnei  23430  unconn  23595  comppfsc  23698  kqsat  23897  isr0  23903  qtophmeo  23983  trufil  24076  alexsubALT  24217  cnextcn  24233  ucnima  24446  iducn  24448  bl2in  24566  addcnlem  25031  rescncf  25065  ovoliunlem2  25671  voliun  25722  mbflimsup  25834  itgcn  26013  dvdsq1p  26329  aalioulem2  26505  recosf1o  26709  logrec  26937  xrlimcnp  27142  basellem4  27257  bposlem1  27457  bposlem5  27461  lgsqrmod  27525  lgsdchrval  27527  2lgslem1a1  27562  pntlem3  27782  nosupbnd1  27887  noinfbnd1  27902  oldbday  28103  lrcut  28106  abslts  28451  n0ssoldg  28555  zsoring  28611  bdayfinbndlem1  28669  isplng  29069  brbtwn2  29264  axbtwnid  29298  elntg2  29344  umgredgprv  29466  umgrpredgv  29499  usgredgprvALT  29554  fusgrfisstep  29688  fusgrfis  29689  nbupgr  29703  nbumgrvtx  29705  finsumvtxdg2size  29909  wlkp1lem8  30037  upgr2pthnlp  30090  wwlksnextinj  30257  usgr2wspthons3  30325  clwwlkccatlem  30349  clwlkclwwlklem2a1  30352  clwwisshclwws  30375  wwlksext2clwwlk  30417  clwwlknonex2lem2  30468  eucrctshift  30603  eucrct2eupth  30605  numclwwlk2lem1  30736  numclwwlk5lem  30747  frgrreggt1  30753  frgrreg  30754  friendship  30759  blocn2  31169  htthlem  31278  axhcompl-zf  31359  spanuni  31905  spansncol  31929  spansneleq  31931  elspansn5  31935  idcnop  32342  pjnormssi  32529  dmdmd  32661  n0nsnel  32870  ifeqeqx  32897  opabssi  32967  ac6mapd  32977  ressupprn  33044  supxrnemnf  33122  rexdiv  33254  xrstos  33339  cnre2csqlem  34309  fsumcvg4  34349  lmxrge0  34351  qqhval2lem  34380  esumpr2  34466  esumcvg  34485  issgon  34522  measxun2  34609  measres  34621  measdivcst  34623  measdivcstALTV  34624  elorrvc  34863  signsply0  34947  bnj580  35310  fnfvintima  35485  nummin  35493  axprALT2  35512  kardfi  35591  0nn0m1nnn0  35612  umgracycusgr  35654  erdsze2lem2  35704  cvmsval  35766  fmlasuc  35886  fundmpss  36267  dfon2lem3  36283  dfrdg4  36451  cgrtriv  36502  btwntriv2  36512  ifscgr  36544  lineext  36576  btwnconn1lem12  36598  colinbtwnle  36618  elicc3  36856  ontgval  36970  onsucconni  36976  axtco1from2  37014  axtcond  37017  axnulregtco  37019  dfttc4lem2  37068  bj-bibibi  37207  bj-cbvalvv  37289  bj-cbval  37296  bj-cbvex  37297  bj-cbvexw  37327  bj-nnf-cbval  37433  bj-equsal  37489  bj-gabeqd  37601  bj-restn0  37760  bj-snmoore  37783  cgsex2gd  37809  bj-elsn0  37827  bj-finsumval0  37957  relowlssretop  38037  sucneqond  38039  finxpsuc  38072  pibt2  38091  wl-nfs1t  38220  finixpnum  38284  ltflcei  38287  matunitlindflem1  38295  poimirlem23  38322  poimirlem24  38323  poimirlem27  38326  poimirlem32  38331  itg2addnclem  38350  areacirclem2  38388  areacirclem5  38391  areacirc  38392  nninfnub  38430  prdstotbnd  38473  heiborlem4  38493  heibor  38500  elghomlem2OLD  38565  grpokerinj  38572  isidlc  38694  disjlem17  39579  prtlem17  39678  dral1-o  39706  axc16g-o  39736  lsator0sp  39803  atlrelat1  40123  cvratlem  40223  diaintclN  41860  dibintclN  41969  cdlemn11pre  42012  dihord2pre  42027  dihintcl  42146  dochkrshp4  42191  lcfrlem9  42352  lcfrlem21  42365  mapdh8e  42586  aks4d1p5  42875  aks6d1c1p1  42902  sticksstones4  42944  0prjspnrel  43387  elrfirn2  43455  rencldnfilem  43575  onsupnmax  43983  onov0suclim  44029  oege1  44061  cantnfresb  44079  dflim5  44084  omabs2  44087  refimssco  44361  rtrclex  44371  intimasn  44411  ss2iundf  44413  ov2ssiunov2  44454  comptiunov2i  44460  iunrelexpuztr  44473  dssmapf1od  44775  mnringmulrcld  44980  mnuprdlem1  45010  mnuprdlem2  45011  snelpwrVD  45567  en3lplem1VD  45579  en3lpVD  45581  orbi1rVD  45584  sbc3orgVD  45587  3impexpVD  45592  equncomVD  45604  trsbcVD  45613  trintALTVD  45616  trintALT  45617  csbingVD  45620  csbsngVD  45629  csbxpgVD  45630  csbrngVD  45632  csbfv12gALTVD  45635  relopabVD  45637  e2ebindVD  45648  xlimpnfxnegmnf  46556  xlimbr  46569  stoweidlem35  46777  stoweidlem48  46790  ormkglobd  47619  cjnpoly  47654  tannpoly  47655  n0nsn2el  47790  rexrsb  47865  2reu8i  47878  funbrafv  47923  rlimdmafv  47942  tz6.12c-afv2  48007  rlimdmafv2  48023  fzopredsuc  48089  2ffzoeq  48093  m1modnep2mod  48123  2timesltsq  48143  eqfvelsetpreimafv  48170  iccpartlt  48201  proththd  48394  even3prm2  48512  fppr2odd  48524  sbgoldbm  48577  nnsum3primesle9  48587  wtgoldbnnsum4prm  48595  bgoldbnnsum3prm  48597  grtrif1o  48735  mgm2mgm  49020  2zrngnmlid  49048  2zrngnmrid  49049  ellcoellss  49243  nneop  49334  fldivexpfllog2  49373  digexp  49415  reorelicc  49518  2itscp  49589  oppc1stflem  50093  prsthinc  50270  elpglem2  50518