Theorem biimprd 247

Description: Deduce a converse implication from a logical equivalence. Deduction associated with biimpr 219 and biimpri 227. (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 245	1 ⊢ (𝜑 → (𝜒 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  syl6bir  254  mpbird  257  sylibrd  259  sylbird  260  con4bid  317  mtbid  324  mtbii  326  imbi1d  342  biimpar  479  prlem1  1054  alexbii  1836  speivw  1978  spfw  2037  cbvalw  2039  alcomiw  2047  cbvalv1  2338  cbval  2398  axc16i  2436  sb3  2477  sb2  2479  axc16gALT  2490  eqrdav  2732  ralbida  3268  rspcimdv  3603  rspcedv  3606  moi2  3713  moi  3715  sspsstr  4106  2nreu  4442  rabsnifsb  4727  ralxfr2d  5409  axprlem4  5425  sbcop1  5489  isso2i  5624  wefrc  5671  elinxp  6020  sotri3  6132  oneqmini  6417  ordsssuc2  6456  ordtri2or  6463  iotan0  6534  2elresin  6672  f1ocnv  6846  tz6.12cOLD  6919  fveqres  6939  fvun1  6983  dffo4  7105  funopsn  7146  fconst5  7207  fnprb  7210  fntpb  7211  isores3  7332  f1owe  7350  weniso  7351  ndmovordi  7598  abnexg  7743  ordsuc  7801  orduniorsuc  7818  ordzsl  7834  tfinds  7849  dmfexALT  7901  f1oweALT  7959  opreuopreu  8020  fnse  8119  poxp3  8136  poseq  8144  soseq  8145  tposfo2  8234  fprlem1  8285  wfrlem5OLD  8313  wfrlem12OLD  8320  issmo2  8349  iordsmo  8357  smoel2  8363  tz7.48lem  8441  oawordeulem  8554  om00  8575  omlimcl  8578  odi  8579  nnawordi  8621  unfi  9172  php2  9211  fiint  9324  fipreima  9358  dffi2  9418  suplub2  9456  wemapsolem  9545  unwdomg  9579  inf3lem3  9625  trcl  9723  frrlem15  9752  fidomtri  9988  prdom2  10001  cardaleph  10084  ackbij1lem16  10230  coflim  10256  coftr  10268  infpssrlem4  10301  isfin7-2  10391  axdc3lem2  10446  axdc3lem4  10448  brdom6disj  10527  entric  10552  fpwwe2lem11  10636  inatsk  10773  grur1a  10814  indpi  10902  reclem3pr  11044  supsrlem  11106  lelttr  11304  dedekindle  11378  negn0  11643  fimaxre  12158  fiminre  12161  nnmulcl  12236  arch  12469  nnnegz  12561  zle0orge1  12575  zeo  12648  uzm1  12860  rpneg  13006  xrlttri  13118  xrlelttr  13135  iccid  13369  icoshft  13450  fzen  13518  elfz1b  13570  elfz2nn0  13592  fleqceilz  13819  zmodidfzoimp  13866  modsumfzodifsn  13909  hasheqf1oi  14311  hashnfinnn0  14321  hashle2prv  14439  swrd0  14608  pfxccatin12lem2  14681  swrdccat  14685  swrdccat3blem  14689  repswswrd  14734  trclublem  14942  max0add  15257  abslt  15261  absle  15262  rexuzre  15299  caurcvg  15623  caucvg  15625  dvdsval2  16200  negdvdsb  16216  muldvds2  16225  dvdsabseq  16256  smuval2  16423  smupvallem  16424  rplpwr  16499  alginv  16512  algfx  16517  coprmgcdb  16586  divgcdcoprm0  16602  oddprmgt2  16636  rpexp1i  16660  qnumdencl  16675  phiprmpw  16709  prmdiveq  16719  prm23lt5  16747  pcmpt  16825  infpnlem1  16843  prmgaplem3  16986  prmgaplem8  16991  imasaddfnlem  17474  plelttr  18297  lubval  18309  lublecllem  18313  glbval  18322  mndind  18709  mndodconglem  19409  sdrgacs  20417  elfrlmbasn0  21318  mavmulsolcl  22053  slesolex  22184  fvmptnn04if  22351  chfacfisf  22356  chfacfisfcpmat  22357  cnpnei  22768  unconn  22933  comppfsc  23036  kqsat  23235  isr0  23241  qtophmeo  23321  trufil  23414  alexsubALT  23555  cnextcn  23571  ucnima  23786  iducn  23788  bl2in  23906  addcnlem  24380  rescncf  24413  ovoliunlem2  25020  voliun  25071  mbflimsup  25183  itgcn  25362  dvdsq1p  25678  aalioulem2  25846  recosf1o  26044  logrec  26268  xrlimcnp  26473  basellem4  26588  bposlem1  26787  bposlem5  26791  lgsqrmod  26855  lgsdchrval  26857  2lgslem1a1  26892  pntlem3  27112  nosupbnd1  27217  noinfbnd1  27232  oldbday  27396  lrcut  27398  brbtwn2  28194  axbtwnid  28228  elntg2  28274  umgredgprv  28398  umgrpredgv  28431  usgredgprvALT  28483  fusgrfisstep  28617  fusgrfis  28618  nbupgr  28632  nbumgrvtx  28634  finsumvtxdg2size  28838  wlkp1lem8  28968  upgr2pthnlp  29020  wwlksnextinj  29184  usgr2wspthons3  29249  clwwlkccatlem  29273  clwlkclwwlklem2a1  29276  clwwisshclwws  29299  wwlksext2clwwlk  29341  clwwlknonex2lem2  29392  eucrctshift  29527  eucrct2eupth  29529  numclwwlk2lem1  29660  numclwwlk5lem  29671  frgrreggt1  29677  frgrreg  29678  friendship  29683  blocn2  30092  htthlem  30201  axhcompl-zf  30282  spanuni  30828  spansncol  30852  spansneleq  30854  elspansn5  30858  idcnop  31265  pjnormssi  31452  dmdmd  31584  bian1d  31731  ifeqeqx  31805  opabssi  31873  ressupprn  31943  supxrnemnf  32012  rexdiv  32123  xrstos  32211  xrge0omnd  32260  cnre2csqlem  32921  fsumcvg4  32961  lmxrge0  32963  qqhval2lem  32992  esumpr2  33096  esumcvg  33115  issgon  33152  measxun2  33239  measres  33251  measdivcst  33253  measdivcstALTV  33254  elorrvc  33493  signsply0  33593  bnj580  33955  nummin  34125  0nn0m1nnn0  34133  umgracycusgr  34176  erdsze2lem2  34226  cvmsval  34288  fmlasuc  34408  fundmpss  34769  dfon2lem3  34788  dfrdg4  34954  cgrtriv  35005  btwntriv2  35015  ifscgr  35047  lineext  35079  btwnconn1lem12  35101  colinbtwnle  35121  elicc3  35250  ontgval  35364  onsucconni  35370  bj-bibibi  35512  bj-cbval  35574  bj-cbvex  35575  bj-cbvexw  35601  bj-equsal  35752  bj-gabeqd  35865  bj-restn0  36019  bj-snmoore  36042  bj-elsn0  36084  bj-finsumval0  36214  relowlssretop  36292  sucneqond  36294  finxpsuc  36327  pibt2  36346  wl-nfs1t  36454  finixpnum  36521  ltflcei  36524  matunitlindflem1  36532  poimirlem23  36559  poimirlem24  36560  poimirlem27  36563  poimirlem32  36568  itg2addnclem  36587  areacirclem2  36625  areacirclem5  36628  areacirc  36629  nninfnub  36667  prdstotbnd  36710  heiborlem4  36730  heibor  36737  elghomlem2OLD  36802  grpokerinj  36809  isidlc  36931  disjlem17  37717  prtlem17  37794  dral1-o  37822  axc16g-o  37852  lsator0sp  37919  atlrelat1  38239  cvratlem  38340  diaintclN  39977  dibintclN  40086  cdlemn11pre  40129  dihord2pre  40144  dihintcl  40263  dochkrshp4  40308  lcfrlem9  40469  lcfrlem21  40482  mapdh8e  40703  aks4d1p5  40993  sticksstones4  41013  metakunt29  41061  0prjspnrel  41417  elrfirn2  41482  rencldnfilem  41606  onsupnmax  42025  onov0suclim  42072  oege1  42104  cantnfresb  42122  dflim5  42127  omabs2  42130  refimssco  42406  rtrclex  42416  intimasn  42456  ss2iundf  42458  ov2ssiunov2  42499  comptiunov2i  42505  iunrelexpuztr  42518  dssmapf1od  42820  mnringmulrcld  43035  mnuprdlem1  43079  mnuprdlem2  43080  snelpwrVD  43640  en3lplem1VD  43652  en3lpVD  43654  orbi1rVD  43657  sbc3orgVD  43660  3impexpVD  43665  equncomVD  43677  trsbcVD  43686  trintALTVD  43689  trintALT  43690  csbingVD  43693  csbsngVD  43702  csbxpgVD  43703  csbrngVD  43705  csbfv12gALTVD  43708  relopabVD  43710  e2ebindVD  43721  xlimpnfxnegmnf  44578  xlimbr  44591  stoweidlem35  44799  stoweidlem48  44812  n0nsn2el  45783  rexrsb  45856  2reu8i  45869  funbrafv  45914  rlimdmafv  45933  tz6.12c-afv2  45998  rlimdmafv2  46014  fzopredsuc  46079  fzoopth  46083  2ffzoeq  46084  eqfvelsetpreimafv  46109  iccpartlt  46140  proththd  46330  even3prm2  46435  fppr2odd  46447  sbgoldbm  46500  nnsum3primesle9  46510  wtgoldbnnsum4prm  46518  bgoldbnnsum3prm  46520  mgm2mgm  46685  2zrngnmlid  46895  2zrngnmrid  46896  ellcoellss  47164  nneop  47260  fldivexpfllog2  47299  digexp  47341  reorelicc  47444  2itscp  47515  prsthinc  47722  elpglem2  47805