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  1835  speivw  1975  spfw  2035  cbvalw  2037  alcomimw  2045  cbvalv1  2346  cbval  2403  axc16i  2441  sb3  2482  sb2  2484  axc16gALT  2495  eqrdav  2736  ralbida  3248  rspcimdv  3567  rspcedv  3570  moi2  3675  moi  3677  sspsstr  4061  2nreu  4397  rabsnifsb  4680  ralxfr2d  5356  axprlem4OLD  5375  sbcop1  5437  isso2i  5570  wefrc  5619  elinxp  5979  sotri3  6088  oneqmini  6371  ordsssuc2  6411  ordtri2or  6418  iotan0  6483  2elresin  6614  f1ocnv  6787  fveqres  6879  fvun1  6926  dffo4  7050  funopsn  7095  fconst5  7154  fnprb  7156  fntpb  7157  isores3  7283  f1owe  7301  weniso  7302  ndmovordi  7551  abnexg  7703  ordsuc  7758  orduniorsuc  7774  ordzsl  7789  tfinds  7804  dmfexALT  7852  f1oweALT  7918  opreuopreu  7980  fnse  8077  poxp3  8094  poseq  8102  soseq  8103  tposfo2  8193  fprlem1  8244  issmo2  8283  iordsmo  8291  smoel2  8297  tz7.48lem  8374  oawordeulem  8483  om00  8504  omlimcl  8507  odi  8508  nnawordi  8551  unfi  9099  php2  9136  fiint  9231  fipreima  9262  dffi2  9330  suplub2  9368  wemapsolem  9459  unwdomg  9493  inf3lem3  9543  trcl  9641  frrlem15  9673  fidomtri  9909  prdom2  9920  cardaleph  10003  ackbij1lem16  10148  coflim  10175  coftr  10187  infpssrlem4  10220  isfin7-2  10310  axdc3lem2  10365  axdc3lem4  10367  brdom6disj  10446  entric  10471  fpwwe2lem11  10556  inatsk  10693  grur1a  10734  indpi  10822  reclem3pr  10964  supsrlem  11026  lelttr  11227  dedekindle  11301  negn0  11570  fimaxre  12090  fiminre  12093  nnmulcl  12173  arch  12402  nnnegz  12495  zle0orge1  12509  zeo  12582  uzm1  12789  rpneg  12943  xrlttri  13057  xrlelttr  13074  iccid  13310  icoshft  13393  fzen  13461  elfz1b  13513  fzdif1  13525  elfz2nn0  13538  fzoopth  13682  fleqceilz  13778  zmodidfzoimp  13825  modsumfzodifsn  13871  hasheqf1oi  14278  hashnfinnn0  14288  hashle2prv  14405  swrd0  14586  pfxccatin12lem2  14658  swrdccat  14662  swrdccat3blem  14666  repswswrd  14711  trclublem  14922  max0add  15237  abslt  15242  absle  15243  rexuzre  15280  caurcvg  15604  caucvg  15606  dvdsval2  16186  negdvdsb  16203  muldvds2  16212  dvdsabseq  16244  smuval2  16413  smupvallem  16414  rplpwr  16489  alginv  16506  algfx  16511  coprmgcdb  16580  divgcdcoprm0  16596  oddprmgt2  16630  rpexp1i  16654  qnumdencl  16670  phiprmpw  16707  prmdiveq  16717  prm23lt5  16746  pcmpt  16824  infpnlem1  16842  prmgaplem3  16985  prmgaplem8  16990  imasaddfnlem  17453  plelttr  18269  lubval  18281  lublecllem  18285  glbval  18294  mndind  18757  mndodconglem  19474  sdrgacs  20738  xrge0omnd  21404  elfrlmbasn0  21722  mavmulsolcl  22499  slesolex  22630  fvmptnn04if  22797  chfacfisf  22802  chfacfisfcpmat  22803  cnpnei  23212  unconn  23377  comppfsc  23480  kqsat  23679  isr0  23685  qtophmeo  23765  trufil  23858  alexsubALT  23999  cnextcn  24015  ucnima  24228  iducn  24230  bl2in  24348  addcnlem  24813  rescncf  24850  ovoliunlem2  25464  voliun  25515  mbflimsup  25627  itgcn  25806  dvdsq1p  26128  aalioulem2  26301  recosf1o  26504  logrec  26733  xrlimcnp  26938  basellem4  27054  bposlem1  27255  bposlem5  27259  lgsqrmod  27323  lgsdchrval  27325  2lgslem1a1  27360  pntlem3  27580  nosupbnd1  27686  noinfbnd1  27701  oldbday  27901  lrcut  27904  abslts  28249  n0ssoldg  28353  zsoring  28409  bdayfinbndlem1  28467  brbtwn2  28982  axbtwnid  29016  elntg2  29062  umgredgprv  29184  umgrpredgv  29217  usgredgprvALT  29272  fusgrfisstep  29406  fusgrfis  29407  nbupgr  29421  nbumgrvtx  29423  finsumvtxdg2size  29628  wlkp1lem8  29756  upgr2pthnlp  29809  wwlksnextinj  29976  usgr2wspthons3  30044  clwwlkccatlem  30068  clwlkclwwlklem2a1  30071  clwwisshclwws  30094  wwlksext2clwwlk  30136  clwwlknonex2lem2  30187  eucrctshift  30322  eucrct2eupth  30324  numclwwlk2lem1  30455  numclwwlk5lem  30466  frgrreggt1  30472  frgrreg  30473  friendship  30478  blocn2  30887  htthlem  30996  axhcompl-zf  31077  spanuni  31623  spansncol  31647  spansneleq  31649  elspansn5  31653  idcnop  32060  pjnormssi  32247  dmdmd  32379  bian1dOLD  32534  n0nsnel  32593  ifeqeqx  32620  opabssi  32694  ac6mapd  32704  ressupprn  32771  supxrnemnf  32850  rexdiv  33009  xrstos  33094  cnre2csqlem  34069  fsumcvg4  34109  lmxrge0  34111  qqhval2lem  34140  esumpr2  34226  esumcvg  34245  issgon  34282  measxun2  34369  measres  34381  measdivcst  34383  measdivcstALTV  34384  elorrvc  34623  signsply0  34710  bnj580  35071  nummin  35251  0nn0m1nnn0  35309  umgracycusgr  35350  erdsze2lem2  35400  cvmsval  35462  fmlasuc  35582  fundmpss  35963  dfon2lem3  35979  dfrdg4  36147  cgrtriv  36198  btwntriv2  36208  ifscgr  36240  lineext  36272  btwnconn1lem12  36294  colinbtwnle  36314  elicc3  36513  ontgval  36627  onsucconni  36633  bj-bibibi  36788  bj-cbval  36851  bj-cbvex  36852  bj-cbvexw  36879  bj-equsal  37029  bj-gabeqd  37140  bj-restn0  37297  bj-snmoore  37320  bj-elsn0  37362  bj-finsumval0  37492  relowlssretop  37570  sucneqond  37572  finxpsuc  37605  pibt2  37624  wl-nfs1t  37744  finixpnum  37808  ltflcei  37811  matunitlindflem1  37819  poimirlem23  37846  poimirlem24  37847  poimirlem27  37850  poimirlem32  37855  itg2addnclem  37874  areacirclem2  37912  areacirclem5  37915  areacirc  37916  nninfnub  37954  prdstotbnd  37997  heiborlem4  38017  heibor  38024  elghomlem2OLD  38089  grpokerinj  38096  isidlc  38218  disjlem17  39105  prtlem17  39204  dral1-o  39232  axc16g-o  39262  lsator0sp  39329  atlrelat1  39649  cvratlem  39749  diaintclN  41386  dibintclN  41495  cdlemn11pre  41538  dihord2pre  41553  dihintcl  41672  dochkrshp4  41717  lcfrlem9  41878  lcfrlem21  41891  mapdh8e  42112  aks4d1p5  42402  aks6d1c1p1  42429  sticksstones4  42471  0prjspnrel  42937  elrfirn2  43005  rencldnfilem  43129  onsupnmax  43537  onov0suclim  43583  oege1  43615  cantnfresb  43633  dflim5  43638  omabs2  43641  refimssco  43915  rtrclex  43925  intimasn  43965  ss2iundf  43967  ov2ssiunov2  44008  comptiunov2i  44014  iunrelexpuztr  44027  dssmapf1od  44329  mnringmulrcld  44536  mnuprdlem1  44580  mnuprdlem2  44581  snelpwrVD  45138  en3lplem1VD  45150  en3lpVD  45152  orbi1rVD  45155  sbc3orgVD  45158  3impexpVD  45163  equncomVD  45175  trsbcVD  45184  trintALTVD  45187  trintALT  45188  csbingVD  45191  csbsngVD  45200  csbxpgVD  45201  csbrngVD  45203  csbfv12gALTVD  45206  relopabVD  45208  e2ebindVD  45219  xlimpnfxnegmnf  46125  xlimbr  46138  stoweidlem35  46346  stoweidlem48  46359  ormkglobd  47186  cjnpoly  47202  tannpoly  47203  n0nsn2el  47338  rexrsb  47413  2reu8i  47426  funbrafv  47471  rlimdmafv  47490  tz6.12c-afv2  47555  rlimdmafv2  47571  fzopredsuc  47636  2ffzoeq  47640  m1modnep2mod  47665  eqfvelsetpreimafv  47706  iccpartlt  47737  proththd  47927  even3prm2  48032  fppr2odd  48044  sbgoldbm  48097  nnsum3primesle9  48107  wtgoldbnnsum4prm  48115  bgoldbnnsum3prm  48117  grtrif1o  48255  mgm2mgm  48540  2zrngnmlid  48568  2zrngnmrid  48569  ellcoellss  48748  nneop  48839  fldivexpfllog2  48878  digexp  48920  reorelicc  49023  2itscp  49094  oppc1stflem  49599  prsthinc  49776  elpglem2  50024