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  3240  rspcimdv  3567  rspcedv  3570  moi2  3676  moi  3678  sspsstr  4059  2nreu  4395  rabsnifsb  4674  ralxfr2d  5349  axprlem4OLD  5368  sbcop1  5431  isso2i  5564  wefrc  5613  elinxp  5970  sotri3  6079  oneqmini  6360  ordsssuc2  6400  ordtri2or  6407  iotan0  6472  2elresin  6603  f1ocnv  6776  fveqres  6867  fvun1  6914  dffo4  7037  funopsn  7082  fconst5  7142  fnprb  7144  fntpb  7145  isores3  7272  f1owe  7290  weniso  7291  ndmovordi  7540  abnexg  7692  ordsuc  7747  orduniorsuc  7763  ordzsl  7778  tfinds  7793  dmfexALT  7841  f1oweALT  7907  opreuopreu  7969  fnse  8066  poxp3  8083  poseq  8091  soseq  8092  tposfo2  8182  fprlem1  8233  issmo2  8272  iordsmo  8280  smoel2  8286  tz7.48lem  8363  oawordeulem  8472  om00  8493  omlimcl  8496  odi  8497  nnawordi  8539  unfi  9085  php2  9122  fiint  9216  fiintOLD  9217  fipreima  9248  dffi2  9313  suplub2  9351  wemapsolem  9442  unwdomg  9476  inf3lem3  9526  trcl  9624  frrlem15  9653  fidomtri  9889  prdom2  9900  cardaleph  9983  ackbij1lem16  10128  coflim  10155  coftr  10167  infpssrlem4  10200  isfin7-2  10290  axdc3lem2  10345  axdc3lem4  10347  brdom6disj  10426  entric  10451  fpwwe2lem11  10535  inatsk  10672  grur1a  10713  indpi  10801  reclem3pr  10943  supsrlem  11005  lelttr  11206  dedekindle  11280  negn0  11549  fimaxre  12069  fiminre  12072  nnmulcl  12152  arch  12381  nnnegz  12474  zle0orge1  12488  zeo  12562  uzm1  12773  rpneg  12927  xrlttri  13041  xrlelttr  13058  iccid  13293  icoshft  13376  fzen  13444  elfz1b  13496  fzdif1  13508  elfz2nn0  13521  fzoopth  13665  fleqceilz  13758  zmodidfzoimp  13805  modsumfzodifsn  13851  hasheqf1oi  14258  hashnfinnn0  14268  hashle2prv  14385  swrd0  14565  pfxccatin12lem2  14637  swrdccat  14641  swrdccat3blem  14645  repswswrd  14690  trclublem  14902  max0add  15217  abslt  15222  absle  15223  rexuzre  15260  caurcvg  15584  caucvg  15586  dvdsval2  16166  negdvdsb  16183  muldvds2  16192  dvdsabseq  16224  smuval2  16393  smupvallem  16394  rplpwr  16469  alginv  16486  algfx  16491  coprmgcdb  16560  divgcdcoprm0  16576  oddprmgt2  16610  rpexp1i  16634  qnumdencl  16650  phiprmpw  16687  prmdiveq  16697  prm23lt5  16726  pcmpt  16804  infpnlem1  16822  prmgaplem3  16965  prmgaplem8  16970  imasaddfnlem  17432  plelttr  18248  lubval  18260  lublecllem  18264  glbval  18273  mndind  18702  mndodconglem  19420  sdrgacs  20686  xrge0omnd  21352  elfrlmbasn0  21670  mavmulsolcl  22436  slesolex  22567  fvmptnn04if  22734  chfacfisf  22739  chfacfisfcpmat  22740  cnpnei  23149  unconn  23314  comppfsc  23417  kqsat  23616  isr0  23622  qtophmeo  23702  trufil  23795  alexsubALT  23936  cnextcn  23952  ucnima  24166  iducn  24168  bl2in  24286  addcnlem  24751  rescncf  24788  ovoliunlem2  25402  voliun  25453  mbflimsup  25565  itgcn  25744  dvdsq1p  26066  aalioulem2  26239  recosf1o  26442  logrec  26671  xrlimcnp  26876  basellem4  26992  bposlem1  27193  bposlem5  27197  lgsqrmod  27261  lgsdchrval  27263  2lgslem1a1  27298  pntlem3  27518  nosupbnd1  27624  noinfbnd1  27639  oldbday  27817  lrcut  27820  absslt  28158  zsoring  28303  brbtwn2  28854  axbtwnid  28888  elntg2  28934  umgredgprv  29056  umgrpredgv  29089  usgredgprvALT  29144  fusgrfisstep  29278  fusgrfis  29279  nbupgr  29293  nbumgrvtx  29295  finsumvtxdg2size  29500  wlkp1lem8  29628  upgr2pthnlp  29681  wwlksnextinj  29848  usgr2wspthons3  29913  clwwlkccatlem  29937  clwlkclwwlklem2a1  29940  clwwisshclwws  29963  wwlksext2clwwlk  30005  clwwlknonex2lem2  30056  eucrctshift  30191  eucrct2eupth  30193  numclwwlk2lem1  30324  numclwwlk5lem  30335  frgrreggt1  30341  frgrreg  30342  friendship  30347  blocn2  30756  htthlem  30865  axhcompl-zf  30946  spanuni  31492  spansncol  31516  spansneleq  31518  elspansn5  31522  idcnop  31929  pjnormssi  32116  dmdmd  32248  bian1dOLD  32405  n0nsnel  32464  ifeqeqx  32491  opabssi  32565  ac6mapd  32575  ressupprn  32640  supxrnemnf  32720  rexdiv  32875  xrstos  32973  cnre2csqlem  33893  fsumcvg4  33933  lmxrge0  33935  qqhval2lem  33964  esumpr2  34050  esumcvg  34069  issgon  34106  measxun2  34193  measres  34205  measdivcst  34207  measdivcstALTV  34208  elorrvc  34448  signsply0  34535  bnj580  34896  nummin  35074  0nn0m1nnn0  35106  umgracycusgr  35147  erdsze2lem2  35197  cvmsval  35259  fmlasuc  35379  fundmpss  35760  dfon2lem3  35779  dfrdg4  35945  cgrtriv  35996  btwntriv2  36006  ifscgr  36038  lineext  36070  btwnconn1lem12  36092  colinbtwnle  36112  elicc3  36311  ontgval  36425  onsucconni  36431  bj-bibibi  36580  bj-cbval  36643  bj-cbvex  36644  bj-cbvexw  36670  bj-equsal  36820  bj-gabeqd  36931  bj-restn0  37084  bj-snmoore  37107  bj-elsn0  37149  bj-finsumval0  37279  relowlssretop  37357  sucneqond  37359  finxpsuc  37392  pibt2  37411  wl-nfs1t  37531  finixpnum  37605  ltflcei  37608  matunitlindflem1  37616  poimirlem23  37643  poimirlem24  37644  poimirlem27  37647  poimirlem32  37652  itg2addnclem  37671  areacirclem2  37709  areacirclem5  37712  areacirc  37713  nninfnub  37751  prdstotbnd  37794  heiborlem4  37814  heibor  37821  elghomlem2OLD  37886  grpokerinj  37893  isidlc  38015  disjlem17  38797  prtlem17  38875  dral1-o  38903  axc16g-o  38933  lsator0sp  39000  atlrelat1  39320  cvratlem  39420  diaintclN  41057  dibintclN  41166  cdlemn11pre  41209  dihord2pre  41224  dihintcl  41343  dochkrshp4  41388  lcfrlem9  41549  lcfrlem21  41562  mapdh8e  41783  aks4d1p5  42073  aks6d1c1p1  42100  sticksstones4  42142  0prjspnrel  42620  elrfirn2  42689  rencldnfilem  42813  onsupnmax  43221  onov0suclim  43267  oege1  43299  cantnfresb  43317  dflim5  43322  omabs2  43325  refimssco  43600  rtrclex  43610  intimasn  43650  ss2iundf  43652  ov2ssiunov2  43693  comptiunov2i  43699  iunrelexpuztr  43712  dssmapf1od  44014  mnringmulrcld  44221  mnuprdlem1  44265  mnuprdlem2  44266  snelpwrVD  44824  en3lplem1VD  44836  en3lpVD  44838  orbi1rVD  44841  sbc3orgVD  44844  3impexpVD  44849  equncomVD  44861  trsbcVD  44870  trintALTVD  44873  trintALT  44874  csbingVD  44877  csbsngVD  44886  csbxpgVD  44887  csbrngVD  44889  csbfv12gALTVD  44892  relopabVD  44894  e2ebindVD  44905  xlimpnfxnegmnf  45815  xlimbr  45828  stoweidlem35  46036  stoweidlem48  46049  ormkglobd  46876  cjnpoly  46893  tannpoly  46894  n0nsn2el  47029  rexrsb  47104  2reu8i  47117  funbrafv  47162  rlimdmafv  47181  tz6.12c-afv2  47246  rlimdmafv2  47262  fzopredsuc  47327  2ffzoeq  47331  m1modnep2mod  47356  eqfvelsetpreimafv  47397  iccpartlt  47428  proththd  47618  even3prm2  47723  fppr2odd  47735  sbgoldbm  47788  nnsum3primesle9  47798  wtgoldbnnsum4prm  47806  bgoldbnnsum3prm  47808  grtrif1o  47946  mgm2mgm  48231  2zrngnmlid  48259  2zrngnmrid  48260  ellcoellss  48440  nneop  48531  fldivexpfllog2  48570  digexp  48612  reorelicc  48715  2itscp  48786  oppc1stflem  49292  prsthinc  49469  elpglem2  49717