Theorem biimprd 248

Description: Deduce a converse implication from a logical equivalence. Deduction associated with biimpr 220 and biimpri 228. (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 22	. 2 ⊢ (𝜒 → 𝜒)
2		biimprd.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	imbitrrid 246	1 ⊢ (𝜑 → (𝜒 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  biimtrrdi  254  mpbird  257  sylibrd  259  sylbird  260  con4bid  317  mtbid  324  mtbii  326  imbi1d  341  biimpar  477  prlem1  1054  alexbii  1833  speivw  1973  spfw  2033  cbvalw  2035  alcomimw  2043  cbvalv1  2339  cbval  2396  axc16i  2434  sb3  2475  sb2  2477  axc16gALT  2488  eqrdav  2728  ralbida  3248  rspcimdv  3578  rspcedv  3581  moi2  3687  moi  3689  sspsstr  4071  2nreu  4407  rabsnifsb  4686  ralxfr2d  5365  axprlem4OLD  5384  sbcop1  5448  isso2i  5583  wefrc  5632  elinxp  5990  sotri3  6103  oneqmini  6385  ordsssuc2  6425  ordtri2or  6432  iotan0  6501  2elresin  6639  f1ocnv  6812  tz6.12cOLD  6885  fveqres  6905  fvun1  6952  dffo4  7075  funopsn  7120  fconst5  7180  fnprb  7182  fntpb  7183  isores3  7310  f1owe  7328  weniso  7329  ndmovordi  7580  abnexg  7732  ordsuc  7788  orduniorsuc  7805  ordzsl  7821  tfinds  7836  dmfexALT  7884  f1oweALT  7951  opreuopreu  8013  fnse  8112  poxp3  8129  poseq  8137  soseq  8138  tposfo2  8228  fprlem1  8279  issmo2  8318  iordsmo  8326  smoel2  8332  tz7.48lem  8409  oawordeulem  8518  om00  8539  omlimcl  8542  odi  8543  nnawordi  8585  unfi  9135  php2  9172  fiint  9277  fiintOLD  9278  fipreima  9309  dffi2  9374  suplub2  9412  wemapsolem  9503  unwdomg  9537  inf3lem3  9583  trcl  9681  frrlem15  9710  fidomtri  9946  prdom2  9959  cardaleph  10042  ackbij1lem16  10187  coflim  10214  coftr  10226  infpssrlem4  10259  isfin7-2  10349  axdc3lem2  10404  axdc3lem4  10406  brdom6disj  10485  entric  10510  fpwwe2lem11  10594  inatsk  10731  grur1a  10772  indpi  10860  reclem3pr  11002  supsrlem  11064  lelttr  11264  dedekindle  11338  negn0  11607  fimaxre  12127  fiminre  12130  nnmulcl  12210  arch  12439  nnnegz  12532  zle0orge1  12546  zeo  12620  uzm1  12831  rpneg  12985  xrlttri  13099  xrlelttr  13116  iccid  13351  icoshft  13434  fzen  13502  elfz1b  13554  fzdif1  13566  elfz2nn0  13579  fzoopth  13723  fleqceilz  13816  zmodidfzoimp  13863  modsumfzodifsn  13909  hasheqf1oi  14316  hashnfinnn0  14326  hashle2prv  14443  swrd0  14623  pfxccatin12lem2  14696  swrdccat  14700  swrdccat3blem  14704  repswswrd  14749  trclublem  14961  max0add  15276  abslt  15281  absle  15282  rexuzre  15319  caurcvg  15643  caucvg  15645  dvdsval2  16225  negdvdsb  16242  muldvds2  16251  dvdsabseq  16283  smuval2  16452  smupvallem  16453  rplpwr  16528  alginv  16545  algfx  16550  coprmgcdb  16619  divgcdcoprm0  16635  oddprmgt2  16669  rpexp1i  16693  qnumdencl  16709  phiprmpw  16746  prmdiveq  16756  prm23lt5  16785  pcmpt  16863  infpnlem1  16881  prmgaplem3  17024  prmgaplem8  17029  imasaddfnlem  17491  plelttr  18303  lubval  18315  lublecllem  18319  glbval  18328  mndind  18755  mndodconglem  19471  sdrgacs  20710  elfrlmbasn0  21672  mavmulsolcl  22438  slesolex  22569  fvmptnn04if  22736  chfacfisf  22741  chfacfisfcpmat  22742  cnpnei  23151  unconn  23316  comppfsc  23419  kqsat  23618  isr0  23624  qtophmeo  23704  trufil  23797  alexsubALT  23938  cnextcn  23954  ucnima  24168  iducn  24170  bl2in  24288  addcnlem  24753  rescncf  24790  ovoliunlem2  25404  voliun  25455  mbflimsup  25567  itgcn  25746  dvdsq1p  26068  aalioulem2  26241  recosf1o  26444  logrec  26673  xrlimcnp  26878  basellem4  26994  bposlem1  27195  bposlem5  27199  lgsqrmod  27263  lgsdchrval  27265  2lgslem1a1  27300  pntlem3  27520  nosupbnd1  27626  noinfbnd1  27641  oldbday  27812  lrcut  27815  absslt  28151  brbtwn2  28832  axbtwnid  28866  elntg2  28912  umgredgprv  29034  umgrpredgv  29067  usgredgprvALT  29122  fusgrfisstep  29256  fusgrfis  29257  nbupgr  29271  nbumgrvtx  29273  finsumvtxdg2size  29478  wlkp1lem8  29608  upgr2pthnlp  29662  wwlksnextinj  29829  usgr2wspthons3  29894  clwwlkccatlem  29918  clwlkclwwlklem2a1  29921  clwwisshclwws  29944  wwlksext2clwwlk  29986  clwwlknonex2lem2  30037  eucrctshift  30172  eucrct2eupth  30174  numclwwlk2lem1  30305  numclwwlk5lem  30316  frgrreggt1  30322  frgrreg  30323  friendship  30328  blocn2  30737  htthlem  30846  axhcompl-zf  30927  spanuni  31473  spansncol  31497  spansneleq  31499  elspansn5  31503  idcnop  31910  pjnormssi  32097  dmdmd  32229  bian1dOLD  32386  n0nsnel  32444  ifeqeqx  32471  opabssi  32541  ac6mapd  32549  ressupprn  32613  supxrnemnf  32691  rexdiv  32846  xrstos  32948  xrge0omnd  33025  cnre2csqlem  33900  fsumcvg4  33940  lmxrge0  33942  qqhval2lem  33971  esumpr2  34057  esumcvg  34076  issgon  34113  measxun2  34200  measres  34212  measdivcst  34214  measdivcstALTV  34215  elorrvc  34455  signsply0  34542  bnj580  34903  nummin  35081  0nn0m1nnn0  35100  umgracycusgr  35141  erdsze2lem2  35191  cvmsval  35253  fmlasuc  35373  fundmpss  35754  dfon2lem3  35773  dfrdg4  35939  cgrtriv  35990  btwntriv2  36000  ifscgr  36032  lineext  36064  btwnconn1lem12  36086  colinbtwnle  36106  elicc3  36305  ontgval  36419  onsucconni  36425  bj-bibibi  36574  bj-cbval  36637  bj-cbvex  36638  bj-cbvexw  36664  bj-equsal  36814  bj-gabeqd  36925  bj-restn0  37078  bj-snmoore  37101  bj-elsn0  37143  bj-finsumval0  37273  relowlssretop  37351  sucneqond  37353  finxpsuc  37386  pibt2  37405  wl-nfs1t  37525  finixpnum  37599  ltflcei  37602  matunitlindflem1  37610  poimirlem23  37637  poimirlem24  37638  poimirlem27  37641  poimirlem32  37646  itg2addnclem  37665  areacirclem2  37703  areacirclem5  37706  areacirc  37707  nninfnub  37745  prdstotbnd  37788  heiborlem4  37808  heibor  37815  elghomlem2OLD  37880  grpokerinj  37887  isidlc  38009  disjlem17  38791  prtlem17  38869  dral1-o  38897  axc16g-o  38927  lsator0sp  38994  atlrelat1  39314  cvratlem  39415  diaintclN  41052  dibintclN  41161  cdlemn11pre  41204  dihord2pre  41219  dihintcl  41338  dochkrshp4  41383  lcfrlem9  41544  lcfrlem21  41557  mapdh8e  41778  aks4d1p5  42068  aks6d1c1p1  42095  sticksstones4  42137  0prjspnrel  42615  elrfirn2  42684  rencldnfilem  42808  onsupnmax  43217  onov0suclim  43263  oege1  43295  cantnfresb  43313  dflim5  43318  omabs2  43321  refimssco  43596  rtrclex  43606  intimasn  43646  ss2iundf  43648  ov2ssiunov2  43689  comptiunov2i  43695  iunrelexpuztr  43708  dssmapf1od  44010  mnringmulrcld  44217  mnuprdlem1  44261  mnuprdlem2  44262  snelpwrVD  44820  en3lplem1VD  44832  en3lpVD  44834  orbi1rVD  44837  sbc3orgVD  44840  3impexpVD  44845  equncomVD  44857  trsbcVD  44866  trintALTVD  44869  trintALT  44870  csbingVD  44873  csbsngVD  44882  csbxpgVD  44883  csbrngVD  44885  csbfv12gALTVD  44888  relopabVD  44890  e2ebindVD  44901  xlimpnfxnegmnf  45812  xlimbr  45825  stoweidlem35  46033  stoweidlem48  46046  ormkglobd  46873  cjnpoly  46890  tannpoly  46891  n0nsn2el  47026  rexrsb  47101  2reu8i  47114  funbrafv  47159  rlimdmafv  47178  tz6.12c-afv2  47243  rlimdmafv2  47259  fzopredsuc  47324  2ffzoeq  47328  m1modnep2mod  47353  eqfvelsetpreimafv  47394  iccpartlt  47425  proththd  47615  even3prm2  47720  fppr2odd  47732  sbgoldbm  47785  nnsum3primesle9  47795  wtgoldbnnsum4prm  47803  bgoldbnnsum3prm  47805  grtrif1o  47941  mgm2mgm  48215  2zrngnmlid  48243  2zrngnmrid  48244  ellcoellss  48424  nneop  48515  fldivexpfllog2  48554  digexp  48596  reorelicc  48699  2itscp  48770  oppc1stflem  49276  prsthinc  49453  elpglem2  49701