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  2397  axc16i  2435  sb3  2476  sb2  2478  axc16gALT  2489  eqrdav  2729  ralbida  3249  rspcimdv  3581  rspcedv  3584  moi2  3690  moi  3692  sspsstr  4074  2nreu  4410  rabsnifsb  4689  ralxfr2d  5368  axprlem4OLD  5387  sbcop1  5451  isso2i  5586  wefrc  5635  elinxp  5993  sotri3  6106  oneqmini  6388  ordsssuc2  6428  ordtri2or  6435  iotan0  6504  2elresin  6642  f1ocnv  6815  tz6.12cOLD  6888  fveqres  6908  fvun1  6955  dffo4  7078  funopsn  7123  fconst5  7183  fnprb  7185  fntpb  7186  isores3  7313  f1owe  7331  weniso  7332  ndmovordi  7583  abnexg  7735  ordsuc  7791  orduniorsuc  7808  ordzsl  7824  tfinds  7839  dmfexALT  7887  f1oweALT  7954  opreuopreu  8016  fnse  8115  poxp3  8132  poseq  8140  soseq  8141  tposfo2  8231  fprlem1  8282  issmo2  8321  iordsmo  8329  smoel2  8335  tz7.48lem  8412  oawordeulem  8521  om00  8542  omlimcl  8545  odi  8546  nnawordi  8588  unfi  9141  php2  9178  fiint  9284  fiintOLD  9285  fipreima  9316  dffi2  9381  suplub2  9419  wemapsolem  9510  unwdomg  9544  inf3lem3  9590  trcl  9688  frrlem15  9717  fidomtri  9953  prdom2  9966  cardaleph  10049  ackbij1lem16  10194  coflim  10221  coftr  10233  infpssrlem4  10266  isfin7-2  10356  axdc3lem2  10411  axdc3lem4  10413  brdom6disj  10492  entric  10517  fpwwe2lem11  10601  inatsk  10738  grur1a  10779  indpi  10867  reclem3pr  11009  supsrlem  11071  lelttr  11271  dedekindle  11345  negn0  11614  fimaxre  12134  fiminre  12137  nnmulcl  12217  arch  12446  nnnegz  12539  zle0orge1  12553  zeo  12627  uzm1  12838  rpneg  12992  xrlttri  13106  xrlelttr  13123  iccid  13358  icoshft  13441  fzen  13509  elfz1b  13561  fzdif1  13573  elfz2nn0  13586  fzoopth  13730  fleqceilz  13823  zmodidfzoimp  13870  modsumfzodifsn  13916  hasheqf1oi  14323  hashnfinnn0  14333  hashle2prv  14450  swrd0  14630  pfxccatin12lem2  14703  swrdccat  14707  swrdccat3blem  14711  repswswrd  14756  trclublem  14968  max0add  15283  abslt  15288  absle  15289  rexuzre  15326  caurcvg  15650  caucvg  15652  dvdsval2  16232  negdvdsb  16249  muldvds2  16258  dvdsabseq  16290  smuval2  16459  smupvallem  16460  rplpwr  16535  alginv  16552  algfx  16557  coprmgcdb  16626  divgcdcoprm0  16642  oddprmgt2  16676  rpexp1i  16700  qnumdencl  16716  phiprmpw  16753  prmdiveq  16763  prm23lt5  16792  pcmpt  16870  infpnlem1  16888  prmgaplem3  17031  prmgaplem8  17036  imasaddfnlem  17498  plelttr  18310  lubval  18322  lublecllem  18326  glbval  18335  mndind  18762  mndodconglem  19478  sdrgacs  20717  elfrlmbasn0  21679  mavmulsolcl  22445  slesolex  22576  fvmptnn04if  22743  chfacfisf  22748  chfacfisfcpmat  22749  cnpnei  23158  unconn  23323  comppfsc  23426  kqsat  23625  isr0  23631  qtophmeo  23711  trufil  23804  alexsubALT  23945  cnextcn  23961  ucnima  24175  iducn  24177  bl2in  24295  addcnlem  24760  rescncf  24797  ovoliunlem2  25411  voliun  25462  mbflimsup  25574  itgcn  25753  dvdsq1p  26075  aalioulem2  26248  recosf1o  26451  logrec  26680  xrlimcnp  26885  basellem4  27001  bposlem1  27202  bposlem5  27206  lgsqrmod  27270  lgsdchrval  27272  2lgslem1a1  27307  pntlem3  27527  nosupbnd1  27633  noinfbnd1  27648  oldbday  27819  lrcut  27822  absslt  28158  brbtwn2  28839  axbtwnid  28873  elntg2  28919  umgredgprv  29041  umgrpredgv  29074  usgredgprvALT  29129  fusgrfisstep  29263  fusgrfis  29264  nbupgr  29278  nbumgrvtx  29280  finsumvtxdg2size  29485  wlkp1lem8  29615  upgr2pthnlp  29669  wwlksnextinj  29836  usgr2wspthons3  29901  clwwlkccatlem  29925  clwlkclwwlklem2a1  29928  clwwisshclwws  29951  wwlksext2clwwlk  29993  clwwlknonex2lem2  30044  eucrctshift  30179  eucrct2eupth  30181  numclwwlk2lem1  30312  numclwwlk5lem  30323  frgrreggt1  30329  frgrreg  30330  friendship  30335  blocn2  30744  htthlem  30853  axhcompl-zf  30934  spanuni  31480  spansncol  31504  spansneleq  31506  elspansn5  31510  idcnop  31917  pjnormssi  32104  dmdmd  32236  bian1dOLD  32393  n0nsnel  32451  ifeqeqx  32478  opabssi  32548  ac6mapd  32556  ressupprn  32620  supxrnemnf  32698  rexdiv  32853  xrstos  32955  xrge0omnd  33032  cnre2csqlem  33907  fsumcvg4  33947  lmxrge0  33949  qqhval2lem  33978  esumpr2  34064  esumcvg  34083  issgon  34120  measxun2  34207  measres  34219  measdivcst  34221  measdivcstALTV  34222  elorrvc  34462  signsply0  34549  bnj580  34910  nummin  35088  0nn0m1nnn0  35107  umgracycusgr  35148  erdsze2lem2  35198  cvmsval  35260  fmlasuc  35380  fundmpss  35761  dfon2lem3  35780  dfrdg4  35946  cgrtriv  35997  btwntriv2  36007  ifscgr  36039  lineext  36071  btwnconn1lem12  36093  colinbtwnle  36113  elicc3  36312  ontgval  36426  onsucconni  36432  bj-bibibi  36581  bj-cbval  36644  bj-cbvex  36645  bj-cbvexw  36671  bj-equsal  36821  bj-gabeqd  36932  bj-restn0  37085  bj-snmoore  37108  bj-elsn0  37150  bj-finsumval0  37280  relowlssretop  37358  sucneqond  37360  finxpsuc  37393  pibt2  37412  wl-nfs1t  37532  finixpnum  37606  ltflcei  37609  matunitlindflem1  37617  poimirlem23  37644  poimirlem24  37645  poimirlem27  37648  poimirlem32  37653  itg2addnclem  37672  areacirclem2  37710  areacirclem5  37713  areacirc  37714  nninfnub  37752  prdstotbnd  37795  heiborlem4  37815  heibor  37822  elghomlem2OLD  37887  grpokerinj  37894  isidlc  38016  disjlem17  38798  prtlem17  38876  dral1-o  38904  axc16g-o  38934  lsator0sp  39001  atlrelat1  39321  cvratlem  39422  diaintclN  41059  dibintclN  41168  cdlemn11pre  41211  dihord2pre  41226  dihintcl  41345  dochkrshp4  41390  lcfrlem9  41551  lcfrlem21  41564  mapdh8e  41785  aks4d1p5  42075  aks6d1c1p1  42102  sticksstones4  42144  0prjspnrel  42622  elrfirn2  42691  rencldnfilem  42815  onsupnmax  43224  onov0suclim  43270  oege1  43302  cantnfresb  43320  dflim5  43325  omabs2  43328  refimssco  43603  rtrclex  43613  intimasn  43653  ss2iundf  43655  ov2ssiunov2  43696  comptiunov2i  43702  iunrelexpuztr  43715  dssmapf1od  44017  mnringmulrcld  44224  mnuprdlem1  44268  mnuprdlem2  44269  snelpwrVD  44827  en3lplem1VD  44839  en3lpVD  44841  orbi1rVD  44844  sbc3orgVD  44847  3impexpVD  44852  equncomVD  44864  trsbcVD  44873  trintALTVD  44876  trintALT  44877  csbingVD  44880  csbsngVD  44889  csbxpgVD  44890  csbrngVD  44892  csbfv12gALTVD  44895  relopabVD  44897  e2ebindVD  44908  xlimpnfxnegmnf  45819  xlimbr  45832  stoweidlem35  46040  stoweidlem48  46053  ormkglobd  46880  n0nsn2el  47030  rexrsb  47105  2reu8i  47118  funbrafv  47163  rlimdmafv  47182  tz6.12c-afv2  47247  rlimdmafv2  47263  fzopredsuc  47328  2ffzoeq  47332  m1modnep2mod  47357  eqfvelsetpreimafv  47398  iccpartlt  47429  proththd  47619  even3prm2  47724  fppr2odd  47736  sbgoldbm  47789  nnsum3primesle9  47799  wtgoldbnnsum4prm  47807  bgoldbnnsum3prm  47809  grtrif1o  47945  mgm2mgm  48219  2zrngnmlid  48247  2zrngnmrid  48248  ellcoellss  48428  nneop  48519  fldivexpfllog2  48558  digexp  48600  reorelicc  48703  2itscp  48774  oppc1stflem  49280  prsthinc  49457  elpglem2  49705