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  1055  alexbii  1835  speivw  1975  spfw  2035  cbvalw  2037  alcomimw  2045  cbvalv1  2346  cbval  2403  axc16i  2441  sb3  2482  sb2  2484  axc16gALT  2495  eqrdav  2736  ralbida  3249  rspcimdv  3568  rspcedv  3571  moi2  3676  moi  3678  sspsstr  4062  2nreu  4398  rabsnifsb  4681  ralxfr2d  5359  axprlem4OLD  5378  sbcop1  5446  isso2i  5579  wefrc  5628  elinxp  5988  sotri3  6097  oneqmini  6380  ordsssuc2  6420  ordtri2or  6427  iotan0  6492  2elresin  6623  f1ocnv  6796  fveqres  6888  fvun1  6935  dffo4  7059  funopsn  7105  fconst5  7164  fnprb  7166  fntpb  7167  isores3  7293  f1owe  7311  weniso  7312  ndmovordi  7561  abnexg  7713  ordsuc  7768  orduniorsuc  7784  ordzsl  7799  tfinds  7814  dmfexALT  7862  f1oweALT  7928  opreuopreu  7990  fnse  8087  poxp3  8104  poseq  8112  soseq  8113  tposfo2  8203  fprlem1  8254  issmo2  8293  iordsmo  8301  smoel2  8307  tz7.48lem  8384  oawordeulem  8493  om00  8514  omlimcl  8517  odi  8518  nnawordi  8561  unfi  9109  php2  9146  fiint  9241  fipreima  9272  dffi2  9340  suplub2  9378  wemapsolem  9469  unwdomg  9503  inf3lem3  9553  trcl  9651  frrlem15  9683  fidomtri  9919  prdom2  9930  cardaleph  10013  ackbij1lem16  10158  coflim  10185  coftr  10197  infpssrlem4  10230  isfin7-2  10320  axdc3lem2  10375  axdc3lem4  10377  brdom6disj  10456  entric  10481  fpwwe2lem11  10566  inatsk  10703  grur1a  10744  indpi  10832  reclem3pr  10974  supsrlem  11036  lelttr  11237  dedekindle  11311  negn0  11580  fimaxre  12100  fiminre  12103  nnmulcl  12183  arch  12412  nnnegz  12505  zle0orge1  12519  zeo  12592  uzm1  12799  rpneg  12953  xrlttri  13067  xrlelttr  13084  iccid  13320  icoshft  13403  fzen  13471  elfz1b  13523  fzdif1  13535  elfz2nn0  13548  fzoopth  13692  fleqceilz  13788  zmodidfzoimp  13835  modsumfzodifsn  13881  hasheqf1oi  14288  hashnfinnn0  14298  hashle2prv  14415  swrd0  14596  pfxccatin12lem2  14668  swrdccat  14672  swrdccat3blem  14676  repswswrd  14721  trclublem  14932  max0add  15247  abslt  15252  absle  15253  rexuzre  15290  caurcvg  15614  caucvg  15616  dvdsval2  16196  negdvdsb  16213  muldvds2  16222  dvdsabseq  16254  smuval2  16423  smupvallem  16424  rplpwr  16499  alginv  16516  algfx  16521  coprmgcdb  16590  divgcdcoprm0  16606  oddprmgt2  16640  rpexp1i  16664  qnumdencl  16680  phiprmpw  16717  prmdiveq  16727  prm23lt5  16756  pcmpt  16834  infpnlem1  16852  prmgaplem3  16995  prmgaplem8  17000  imasaddfnlem  17463  plelttr  18279  lubval  18291  lublecllem  18295  glbval  18304  mndind  18767  mndodconglem  19487  sdrgacs  20751  xrge0omnd  21417  elfrlmbasn0  21735  mavmulsolcl  22512  slesolex  22643  fvmptnn04if  22810  chfacfisf  22815  chfacfisfcpmat  22816  cnpnei  23225  unconn  23390  comppfsc  23493  kqsat  23692  isr0  23698  qtophmeo  23778  trufil  23871  alexsubALT  24012  cnextcn  24028  ucnima  24241  iducn  24243  bl2in  24361  addcnlem  24826  rescncf  24863  ovoliunlem2  25477  voliun  25528  mbflimsup  25640  itgcn  25819  dvdsq1p  26141  aalioulem2  26314  recosf1o  26517  logrec  26746  xrlimcnp  26951  basellem4  27067  bposlem1  27268  bposlem5  27272  lgsqrmod  27336  lgsdchrval  27338  2lgslem1a1  27373  pntlem3  27593  nosupbnd1  27699  noinfbnd1  27714  oldbday  27914  lrcut  27917  abslts  28262  n0ssoldg  28366  zsoring  28422  bdayfinbndlem1  28480  brbtwn2  28996  axbtwnid  29030  elntg2  29076  umgredgprv  29198  umgrpredgv  29231  usgredgprvALT  29286  fusgrfisstep  29420  fusgrfis  29421  nbupgr  29435  nbumgrvtx  29437  finsumvtxdg2size  29642  wlkp1lem8  29770  upgr2pthnlp  29823  wwlksnextinj  29990  usgr2wspthons3  30058  clwwlkccatlem  30082  clwlkclwwlklem2a1  30085  clwwisshclwws  30108  wwlksext2clwwlk  30150  clwwlknonex2lem2  30201  eucrctshift  30336  eucrct2eupth  30338  numclwwlk2lem1  30469  numclwwlk5lem  30480  frgrreggt1  30486  frgrreg  30487  friendship  30492  blocn2  30902  htthlem  31011  axhcompl-zf  31092  spanuni  31638  spansncol  31662  spansneleq  31664  elspansn5  31668  idcnop  32075  pjnormssi  32262  dmdmd  32394  bian1dOLD  32549  n0nsnel  32608  ifeqeqx  32635  opabssi  32709  ac6mapd  32719  ressupprn  32786  supxrnemnf  32865  rexdiv  33024  xrstos  33109  cnre2csqlem  34094  fsumcvg4  34134  lmxrge0  34136  qqhval2lem  34165  esumpr2  34251  esumcvg  34270  issgon  34307  measxun2  34394  measres  34406  measdivcst  34408  measdivcstALTV  34409  elorrvc  34648  signsply0  34735  bnj580  35095  nummin  35276  axprALT2  35293  0nn0m1nnn0  35335  umgracycusgr  35376  erdsze2lem2  35426  cvmsval  35488  fmlasuc  35608  fundmpss  35989  dfon2lem3  36005  dfrdg4  36173  cgrtriv  36224  btwntriv2  36234  ifscgr  36266  lineext  36298  btwnconn1lem12  36320  colinbtwnle  36340  elicc3  36539  ontgval  36653  onsucconni  36659  bj-bibibi  36819  bj-cbvalvv  36901  bj-cbval  36908  bj-cbvex  36909  bj-cbvexw  36939  bj-nnf-cbval  37045  bj-equsal  37101  bj-gabeqd  37212  bj-restn0  37370  bj-snmoore  37393  cgsex2gd  37419  bj-elsn0  37437  bj-finsumval0  37567  relowlssretop  37645  sucneqond  37647  finxpsuc  37680  pibt2  37699  wl-nfs1t  37821  finixpnum  37885  ltflcei  37888  matunitlindflem1  37896  poimirlem23  37923  poimirlem24  37924  poimirlem27  37927  poimirlem32  37932  itg2addnclem  37951  areacirclem2  37989  areacirclem5  37992  areacirc  37993  nninfnub  38031  prdstotbnd  38074  heiborlem4  38094  heibor  38101  elghomlem2OLD  38166  grpokerinj  38173  isidlc  38295  disjlem17  39182  prtlem17  39281  dral1-o  39309  axc16g-o  39339  lsator0sp  39406  atlrelat1  39726  cvratlem  39826  diaintclN  41463  dibintclN  41572  cdlemn11pre  41615  dihord2pre  41630  dihintcl  41749  dochkrshp4  41794  lcfrlem9  41955  lcfrlem21  41968  mapdh8e  42189  aks4d1p5  42479  aks6d1c1p1  42506  sticksstones4  42548  0prjspnrel  43014  elrfirn2  43082  rencldnfilem  43206  onsupnmax  43614  onov0suclim  43660  oege1  43692  cantnfresb  43710  dflim5  43715  omabs2  43718  refimssco  43992  rtrclex  44002  intimasn  44042  ss2iundf  44044  ov2ssiunov2  44085  comptiunov2i  44091  iunrelexpuztr  44104  dssmapf1od  44406  mnringmulrcld  44613  mnuprdlem1  44657  mnuprdlem2  44658  snelpwrVD  45215  en3lplem1VD  45227  en3lpVD  45229  orbi1rVD  45232  sbc3orgVD  45235  3impexpVD  45240  equncomVD  45252  trsbcVD  45261  trintALTVD  45264  trintALT  45265  csbingVD  45268  csbsngVD  45277  csbxpgVD  45278  csbrngVD  45280  csbfv12gALTVD  45283  relopabVD  45285  e2ebindVD  45296  xlimpnfxnegmnf  46201  xlimbr  46214  stoweidlem35  46422  stoweidlem48  46435  ormkglobd  47262  cjnpoly  47278  tannpoly  47279  n0nsn2el  47414  rexrsb  47489  2reu8i  47502  funbrafv  47547  rlimdmafv  47566  tz6.12c-afv2  47631  rlimdmafv2  47647  fzopredsuc  47712  2ffzoeq  47716  m1modnep2mod  47741  eqfvelsetpreimafv  47782  iccpartlt  47813  proththd  48003  even3prm2  48108  fppr2odd  48120  sbgoldbm  48173  nnsum3primesle9  48183  wtgoldbnnsum4prm  48191  bgoldbnnsum3prm  48193  grtrif1o  48331  mgm2mgm  48616  2zrngnmlid  48644  2zrngnmrid  48645  ellcoellss  48824  nneop  48915  fldivexpfllog2  48954  digexp  48996  reorelicc  49099  2itscp  49170  oppc1stflem  49675  prsthinc  49852  elpglem2  50100