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  1831  speivw  1973  spfw  2032  cbvalw  2034  alcomimw  2042  cbvalv1  2347  cbval  2406  axc16i  2444  sb3  2485  sb2  2487  axc16gALT  2498  eqrdav  2739  ralbida  3276  rspcimdv  3625  rspcedv  3628  moi2  3738  moi  3740  sspsstr  4131  2nreu  4467  rabsnifsb  4747  ralxfr2d  5428  axprlem4  5444  sbcop1  5508  isso2i  5644  wefrc  5694  elinxp  6048  sotri3  6162  oneqmini  6447  ordsssuc2  6486  ordtri2or  6493  iotan0  6563  2elresin  6701  f1ocnv  6874  tz6.12cOLD  6947  fveqres  6967  fvun1  7013  dffo4  7137  funopsn  7182  fconst5  7243  fnprb  7245  fntpb  7246  isores3  7371  f1owe  7389  weniso  7390  ndmovordi  7641  abnexg  7791  ordsuc  7849  orduniorsuc  7866  ordzsl  7882  tfinds  7897  dmfexALT  7948  f1oweALT  8013  opreuopreu  8075  fnse  8174  poxp3  8191  poseq  8199  soseq  8200  tposfo2  8290  fprlem1  8341  wfrlem5OLD  8369  wfrlem12OLD  8376  issmo2  8405  iordsmo  8413  smoel2  8419  tz7.48lem  8497  oawordeulem  8610  om00  8631  omlimcl  8634  odi  8635  nnawordi  8677  unfi  9238  php2  9274  fiint  9394  fiintOLD  9395  fipreima  9428  dffi2  9492  suplub2  9530  wemapsolem  9619  unwdomg  9653  inf3lem3  9699  trcl  9797  frrlem15  9826  fidomtri  10062  prdom2  10075  cardaleph  10158  ackbij1lem16  10303  coflim  10330  coftr  10342  infpssrlem4  10375  isfin7-2  10465  axdc3lem2  10520  axdc3lem4  10522  brdom6disj  10601  entric  10626  fpwwe2lem11  10710  inatsk  10847  grur1a  10888  indpi  10976  reclem3pr  11118  supsrlem  11180  lelttr  11380  dedekindle  11454  negn0  11719  fimaxre  12239  fiminre  12242  nnmulcl  12317  arch  12550  nnnegz  12642  zle0orge1  12656  zeo  12729  uzm1  12941  rpneg  13089  xrlttri  13201  xrlelttr  13218  iccid  13452  icoshft  13533  fzen  13601  elfz1b  13653  elfz2nn0  13675  fzoopth  13812  fleqceilz  13905  zmodidfzoimp  13952  modsumfzodifsn  13995  hasheqf1oi  14400  hashnfinnn0  14410  hashle2prv  14527  swrd0  14706  pfxccatin12lem2  14779  swrdccat  14783  swrdccat3blem  14787  repswswrd  14832  trclublem  15044  max0add  15359  abslt  15363  absle  15364  rexuzre  15401  caurcvg  15725  caucvg  15727  dvdsval2  16305  negdvdsb  16321  muldvds2  16330  dvdsabseq  16361  smuval2  16528  smupvallem  16529  rplpwr  16605  alginv  16622  algfx  16627  coprmgcdb  16696  divgcdcoprm0  16712  oddprmgt2  16746  rpexp1i  16770  qnumdencl  16786  phiprmpw  16823  prmdiveq  16833  prm23lt5  16861  pcmpt  16939  infpnlem1  16957  prmgaplem3  17100  prmgaplem8  17105  imasaddfnlem  17588  plelttr  18414  lubval  18426  lublecllem  18430  glbval  18439  mndind  18863  mndodconglem  19583  sdrgacs  20824  elfrlmbasn0  21806  mavmulsolcl  22578  slesolex  22709  fvmptnn04if  22876  chfacfisf  22881  chfacfisfcpmat  22882  cnpnei  23293  unconn  23458  comppfsc  23561  kqsat  23760  isr0  23766  qtophmeo  23846  trufil  23939  alexsubALT  24080  cnextcn  24096  ucnima  24311  iducn  24313  bl2in  24431  addcnlem  24905  rescncf  24942  ovoliunlem2  25557  voliun  25608  mbflimsup  25720  itgcn  25900  dvdsq1p  26222  aalioulem2  26393  recosf1o  26595  logrec  26824  xrlimcnp  27029  basellem4  27145  bposlem1  27346  bposlem5  27350  lgsqrmod  27414  lgsdchrval  27416  2lgslem1a1  27451  pntlem3  27671  nosupbnd1  27777  noinfbnd1  27792  oldbday  27957  lrcut  27959  absslt  28291  brbtwn2  28938  axbtwnid  28972  elntg2  29018  umgredgprv  29142  umgrpredgv  29175  usgredgprvALT  29230  fusgrfisstep  29364  fusgrfis  29365  nbupgr  29379  nbumgrvtx  29381  finsumvtxdg2size  29586  wlkp1lem8  29716  upgr2pthnlp  29768  wwlksnextinj  29932  usgr2wspthons3  29997  clwwlkccatlem  30021  clwlkclwwlklem2a1  30024  clwwisshclwws  30047  wwlksext2clwwlk  30089  clwwlknonex2lem2  30140  eucrctshift  30275  eucrct2eupth  30277  numclwwlk2lem1  30408  numclwwlk5lem  30419  frgrreggt1  30425  frgrreg  30426  friendship  30431  blocn2  30840  htthlem  30949  axhcompl-zf  31030  spanuni  31576  spansncol  31600  spansneleq  31602  elspansn5  31606  idcnop  32013  pjnormssi  32200  dmdmd  32332  bian1dOLD  32485  n0nsnel  32544  ifeqeqx  32565  opabssi  32635  ressupprn  32702  supxrnemnf  32775  rexdiv  32890  xrstos  32993  xrge0omnd  33061  cnre2csqlem  33856  fsumcvg4  33896  lmxrge0  33898  qqhval2lem  33927  esumpr2  34031  esumcvg  34050  issgon  34087  measxun2  34174  measres  34186  measdivcst  34188  measdivcstALTV  34189  elorrvc  34428  signsply0  34528  bnj580  34889  nummin  35067  0nn0m1nnn0  35080  umgracycusgr  35122  erdsze2lem2  35172  cvmsval  35234  fmlasuc  35354  fundmpss  35730  dfon2lem3  35749  dfrdg4  35915  cgrtriv  35966  btwntriv2  35976  ifscgr  36008  lineext  36040  btwnconn1lem12  36062  colinbtwnle  36082  elicc3  36283  ontgval  36397  onsucconni  36403  bj-bibibi  36552  bj-cbval  36615  bj-cbvex  36616  bj-cbvexw  36642  bj-equsal  36792  bj-gabeqd  36903  bj-restn0  37056  bj-snmoore  37079  bj-elsn0  37121  bj-finsumval0  37251  relowlssretop  37329  sucneqond  37331  finxpsuc  37364  pibt2  37383  wl-nfs1t  37491  finixpnum  37565  ltflcei  37568  matunitlindflem1  37576  poimirlem23  37603  poimirlem24  37604  poimirlem27  37607  poimirlem32  37612  itg2addnclem  37631  areacirclem2  37669  areacirclem5  37672  areacirc  37673  nninfnub  37711  prdstotbnd  37754  heiborlem4  37774  heibor  37781  elghomlem2OLD  37846  grpokerinj  37853  isidlc  37975  disjlem17  38755  prtlem17  38832  dral1-o  38860  axc16g-o  38890  lsator0sp  38957  atlrelat1  39277  cvratlem  39378  diaintclN  41015  dibintclN  41124  cdlemn11pre  41167  dihord2pre  41182  dihintcl  41301  dochkrshp4  41346  lcfrlem9  41507  lcfrlem21  41520  mapdh8e  41741  aks4d1p5  42037  aks6d1c1p1  42064  sticksstones4  42106  metakunt29  42190  0prjspnrel  42582  elrfirn2  42652  rencldnfilem  42776  onsupnmax  43189  onov0suclim  43236  oege1  43268  cantnfresb  43286  dflim5  43291  omabs2  43294  refimssco  43569  rtrclex  43579  intimasn  43619  ss2iundf  43621  ov2ssiunov2  43662  comptiunov2i  43668  iunrelexpuztr  43681  dssmapf1od  43983  mnringmulrcld  44197  mnuprdlem1  44241  mnuprdlem2  44242  snelpwrVD  44802  en3lplem1VD  44814  en3lpVD  44816  orbi1rVD  44819  sbc3orgVD  44822  3impexpVD  44827  equncomVD  44839  trsbcVD  44848  trintALTVD  44851  trintALT  44852  csbingVD  44855  csbsngVD  44864  csbxpgVD  44865  csbrngVD  44867  csbfv12gALTVD  44870  relopabVD  44872  e2ebindVD  44883  xlimpnfxnegmnf  45735  xlimbr  45748  stoweidlem35  45956  stoweidlem48  45969  n0nsn2el  46940  rexrsb  47015  2reu8i  47028  funbrafv  47073  rlimdmafv  47092  tz6.12c-afv2  47157  rlimdmafv2  47173  fzopredsuc  47238  2ffzoeq  47242  eqfvelsetpreimafv  47267  iccpartlt  47298  proththd  47488  even3prm2  47593  fppr2odd  47605  sbgoldbm  47658  nnsum3primesle9  47668  wtgoldbnnsum4prm  47676  bgoldbnnsum3prm  47678  grtrif1o  47793  mgm2mgm  47950  2zrngnmlid  47978  2zrngnmrid  47979  ellcoellss  48164  nneop  48260  fldivexpfllog2  48299  digexp  48341  reorelicc  48444  2itscp  48515  prsthinc  48721  elpglem2  48804