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  1829  speivw  1970  spfw  2029  cbvalw  2031  alcomimw  2039  cbvalv1  2341  cbval  2400  axc16i  2438  sb3  2479  sb2  2481  axc16gALT  2492  eqrdav  2733  ralbida  3267  rspcimdv  3611  rspcedv  3614  moi2  3724  moi  3726  sspsstr  4117  2nreu  4449  rabsnifsb  4726  ralxfr2d  5415  axprlem4OLD  5434  sbcop1  5498  isso2i  5632  wefrc  5682  elinxp  6038  sotri3  6152  oneqmini  6437  ordsssuc2  6476  ordtri2or  6483  iotan0  6552  2elresin  6689  f1ocnv  6860  tz6.12cOLD  6933  fveqres  6953  fvun1  6999  dffo4  7122  funopsn  7167  fconst5  7225  fnprb  7227  fntpb  7228  isores3  7354  f1owe  7372  weniso  7373  ndmovordi  7623  abnexg  7774  ordsuc  7832  orduniorsuc  7849  ordzsl  7865  tfinds  7880  dmfexALT  7930  f1oweALT  7995  opreuopreu  8057  fnse  8156  poxp3  8173  poseq  8181  soseq  8182  tposfo2  8272  fprlem1  8323  wfrlem5OLD  8351  wfrlem12OLD  8358  issmo2  8387  iordsmo  8395  smoel2  8401  tz7.48lem  8479  oawordeulem  8590  om00  8611  omlimcl  8614  odi  8615  nnawordi  8657  unfi  9209  php2  9245  fiint  9363  fiintOLD  9364  fipreima  9395  dffi2  9460  suplub2  9498  wemapsolem  9587  unwdomg  9621  inf3lem3  9667  trcl  9765  frrlem15  9794  fidomtri  10030  prdom2  10043  cardaleph  10126  ackbij1lem16  10271  coflim  10298  coftr  10310  infpssrlem4  10343  isfin7-2  10433  axdc3lem2  10488  axdc3lem4  10490  brdom6disj  10569  entric  10594  fpwwe2lem11  10678  inatsk  10815  grur1a  10856  indpi  10944  reclem3pr  11086  supsrlem  11148  lelttr  11348  dedekindle  11422  negn0  11689  fimaxre  12209  fiminre  12212  nnmulcl  12287  arch  12520  nnnegz  12613  zle0orge1  12627  zeo  12701  uzm1  12913  rpneg  13064  xrlttri  13177  xrlelttr  13194  iccid  13428  icoshft  13509  fzen  13577  elfz1b  13629  fzdif1  13641  elfz2nn0  13654  fzoopth  13797  fleqceilz  13890  zmodidfzoimp  13937  modsumfzodifsn  13981  hasheqf1oi  14386  hashnfinnn0  14396  hashle2prv  14513  swrd0  14692  pfxccatin12lem2  14765  swrdccat  14769  swrdccat3blem  14773  repswswrd  14818  trclublem  15030  max0add  15345  abslt  15349  absle  15350  rexuzre  15387  caurcvg  15709  caucvg  15711  dvdsval2  16289  negdvdsb  16306  muldvds2  16315  dvdsabseq  16346  smuval2  16515  smupvallem  16516  rplpwr  16591  alginv  16608  algfx  16613  coprmgcdb  16682  divgcdcoprm0  16698  oddprmgt2  16732  rpexp1i  16756  qnumdencl  16772  phiprmpw  16809  prmdiveq  16819  prm23lt5  16847  pcmpt  16925  infpnlem1  16943  prmgaplem3  17086  prmgaplem8  17091  imasaddfnlem  17574  plelttr  18401  lubval  18413  lublecllem  18417  glbval  18426  mndind  18853  mndodconglem  19573  sdrgacs  20818  elfrlmbasn0  21800  mavmulsolcl  22572  slesolex  22703  fvmptnn04if  22870  chfacfisf  22875  chfacfisfcpmat  22876  cnpnei  23287  unconn  23452  comppfsc  23555  kqsat  23754  isr0  23760  qtophmeo  23840  trufil  23933  alexsubALT  24074  cnextcn  24090  ucnima  24305  iducn  24307  bl2in  24425  addcnlem  24899  rescncf  24936  ovoliunlem2  25551  voliun  25602  mbflimsup  25714  itgcn  25894  dvdsq1p  26216  aalioulem2  26389  recosf1o  26591  logrec  26820  xrlimcnp  27025  basellem4  27141  bposlem1  27342  bposlem5  27346  lgsqrmod  27410  lgsdchrval  27412  2lgslem1a1  27447  pntlem3  27667  nosupbnd1  27773  noinfbnd1  27788  oldbday  27953  lrcut  27955  absslt  28287  brbtwn2  28934  axbtwnid  28968  elntg2  29014  umgredgprv  29138  umgrpredgv  29171  usgredgprvALT  29226  fusgrfisstep  29360  fusgrfis  29361  nbupgr  29375  nbumgrvtx  29377  finsumvtxdg2size  29582  wlkp1lem8  29712  upgr2pthnlp  29764  wwlksnextinj  29928  usgr2wspthons3  29993  clwwlkccatlem  30017  clwlkclwwlklem2a1  30020  clwwisshclwws  30043  wwlksext2clwwlk  30085  clwwlknonex2lem2  30136  eucrctshift  30271  eucrct2eupth  30273  numclwwlk2lem1  30404  numclwwlk5lem  30415  frgrreggt1  30421  frgrreg  30422  friendship  30427  blocn2  30836  htthlem  30945  axhcompl-zf  31026  spanuni  31572  spansncol  31596  spansneleq  31598  elspansn5  31602  idcnop  32009  pjnormssi  32196  dmdmd  32328  bian1dOLD  32484  n0nsnel  32542  ifeqeqx  32562  opabssi  32632  ressupprn  32704  supxrnemnf  32778  rexdiv  32892  xrstos  32994  xrge0omnd  33070  cnre2csqlem  33870  fsumcvg4  33910  lmxrge0  33912  qqhval2lem  33943  esumpr2  34047  esumcvg  34066  issgon  34103  measxun2  34190  measres  34202  measdivcst  34204  measdivcstALTV  34205  elorrvc  34444  signsply0  34544  bnj580  34905  nummin  35083  0nn0m1nnn0  35096  umgracycusgr  35138  erdsze2lem2  35188  cvmsval  35250  fmlasuc  35370  fundmpss  35747  dfon2lem3  35766  dfrdg4  35932  cgrtriv  35983  btwntriv2  35993  ifscgr  36025  lineext  36057  btwnconn1lem12  36079  colinbtwnle  36099  elicc3  36299  ontgval  36413  onsucconni  36419  bj-bibibi  36568  bj-cbval  36631  bj-cbvex  36632  bj-cbvexw  36658  bj-equsal  36808  bj-gabeqd  36919  bj-restn0  37072  bj-snmoore  37095  bj-elsn0  37137  bj-finsumval0  37267  relowlssretop  37345  sucneqond  37347  finxpsuc  37380  pibt2  37399  wl-nfs1t  37517  finixpnum  37591  ltflcei  37594  matunitlindflem1  37602  poimirlem23  37629  poimirlem24  37630  poimirlem27  37633  poimirlem32  37638  itg2addnclem  37657  areacirclem2  37695  areacirclem5  37698  areacirc  37699  nninfnub  37737  prdstotbnd  37780  heiborlem4  37800  heibor  37807  elghomlem2OLD  37872  grpokerinj  37879  isidlc  38001  disjlem17  38780  prtlem17  38857  dral1-o  38885  axc16g-o  38915  lsator0sp  38982  atlrelat1  39302  cvratlem  39403  diaintclN  41040  dibintclN  41149  cdlemn11pre  41192  dihord2pre  41207  dihintcl  41326  dochkrshp4  41371  lcfrlem9  41532  lcfrlem21  41545  mapdh8e  41766  aks4d1p5  42061  aks6d1c1p1  42088  sticksstones4  42130  metakunt29  42214  0prjspnrel  42613  elrfirn2  42683  rencldnfilem  42807  onsupnmax  43216  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  44223  mnuprdlem1  44267  mnuprdlem2  44268  snelpwrVD  44828  en3lplem1VD  44840  en3lpVD  44842  orbi1rVD  44845  sbc3orgVD  44848  3impexpVD  44853  equncomVD  44865  trsbcVD  44874  trintALTVD  44877  trintALT  44878  csbingVD  44881  csbsngVD  44890  csbxpgVD  44891  csbrngVD  44893  csbfv12gALTVD  44896  relopabVD  44898  e2ebindVD  44909  xlimpnfxnegmnf  45769  xlimbr  45782  stoweidlem35  45990  stoweidlem48  46003  n0nsn2el  46974  rexrsb  47049  2reu8i  47062  funbrafv  47107  rlimdmafv  47126  tz6.12c-afv2  47191  rlimdmafv2  47207  fzopredsuc  47272  2ffzoeq  47276  m1modnep2mod  47291  eqfvelsetpreimafv  47317  iccpartlt  47348  proththd  47538  even3prm2  47643  fppr2odd  47655  sbgoldbm  47708  nnsum3primesle9  47718  wtgoldbnnsum4prm  47726  bgoldbnnsum3prm  47728  grtrif1o  47846  mgm2mgm  48070  2zrngnmlid  48098  2zrngnmrid  48099  ellcoellss  48280  nneop  48375  fldivexpfllog2  48414  digexp  48456  reorelicc  48559  2itscp  48630  prsthinc  48854  elpglem2  48942