Theorem biimprd 251

Description: Deduce a converse implication from a logical equivalence. Deduction associated with biimpr 223 and biimpri 231. (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 23	. 2 ⊢ (𝜒 → 𝜒)
2		biimprd.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	imbitrrid 249	1 ⊢ (𝜑 → (𝜒 → 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  biimtrrdi  257  mpbird  260  sylibrd  262  sylbird  263  con4bid  320  mtbid  327  mtbii  329  imbi1d  344  biimpar  483  prlem1  1070  alexbii  1866  speivw  2006  spfw  2066  cbvalw  2068  alcomimw  2076  cbvalv1  2372  cbval  2429  axc16i  2467  sb3  2508  sb2  2510  axc16gALT  2521  ralbida  3275  rspcimdv  3569  rspcedv  3572  moi2  3677  moi  3679  sspsstr  4060  2nreu  4405  rabsnifsb  4686  ralxfr2d  5379  axprlem4OLD  5399  sbcop1  5468  isso2i  5604  wefrc  5653  elinxp  6016  sotri3  6128  oneqmini  6415  ordsssuc2  6455  ordtri2or  6462  iotan0  6527  2elresin  6657  f1ocnv  6834  fveqres  6926  fvun1  6973  dffo4  7099  funopsnOLD  7148  fconst5  7208  fnprb  7210  fntpb  7211  isores3  7339  f1oweOLD  7358  weniso  7360  ndmovordi  7608  abnexg  7758  ordsuc  7813  orduniorsuc  7829  ordzsl  7844  tfinds  7859  dmfexALT  7908  f1oweALT  7972  opreuopreu  8034  fnse  8134  poxp3  8151  poseq  8159  soseq  8160  tposfo2  8250  fprlem1  8302  issmo2  8341  iordsmo  8349  smoel2  8355  tz7.48lem  8433  oawordeulem  8544  om00  8565  omlimcl  8568  odi  8569  nnawordi  8612  unfi  9168  php2  9205  fiint  9299  fipreima  9328  dffi2  9396  suplub2  9434  wemapsolem  9525  unwdomg  9559  inf3lem3  9612  wemapwe  9679  trcl  9710  frrlem15  9742  fidomtri  10001  prdom2  10012  cardaleph  10095  ackbij1lem16  10239  coflim  10266  coftr  10278  infpssrlem4  10311  isfin7-2  10401  axdc3lem2  10456  axdc3lem4  10458  brdom6disj  10538  entric  10566  fpwwe2lem11  10651  inatsk  10788  grur1a  10829  indpi  10917  reclem3pr  11059  supsrlem  11121  lelttr  11325  dedekindle  11399  negn0  11668  fimaxre  12184  fiminre  12187  nnmulcl  12282  arch  12526  nnnegz  12619  zle0orge1  12633  0nn0m1nnn0  12676  zeo  12708  uzm1  12922  rpneg  13076  xrlttri  13190  xrlelttr  13207  iccid  13443  icoshft  13526  fzen  13595  elfz1b  13648  fzdif1  13660  elfz2nn0  13673  fzoopth  13818  fleqceilz  13915  zmodidfzoimp  13962  modsumfzodifsn  14008  hasheqf1oi  14415  hashnfinnn0  14425  hashle2prv  14543  swrd0  14728  pfxccatin12lem2  14800  swrdccat  14804  swrdccat3blem  14808  repswswrd  14855  trclublem  15068  max0add  15397  abslt  15402  absle  15403  rexuzre  15440  caurcvg  15764  caucvg  15766  dvdsval2  16347  negdvdsb  16364  muldvds2  16373  dvdsabseq  16405  smuval2  16574  smupvallem  16575  rplpwr  16650  alginv  16667  algfx  16672  coprmgcdb  16741  divgcdcoprm0  16757  oddprmgt2  16792  rpexp1i  16816  qnumdencl  16832  phiprmpw  16869  prmdiveq  16879  prm23lt5  16908  pcmpt  16986  infpnlem1  17004  prmgaplem3  17147  prmgaplem8  17152  imasaddfnlem  17616  plelttr  18432  lubval  18444  lublecllem  18448  glbval  18457  mndind  18936  mndodconglem  19667  sdrgacs  20966  xrge0omnd  21657  elfrlmbasn0  21975  mavmulsolcl  22772  matunitlindflem1  22900  slesolex  22906  fvmptnn04if  23073  chfacfisf  23078  chfacfisfcpmat  23079  cnpnei  23488  unconn  23653  comppfsc  23757  kqsat  23956  isr0  23962  qtophmeo  24042  trufil  24135  alexsubALT  24276  cnextcn  24292  ucnima  24505  iducn  24507  bl2in  24625  addcnlem  25090  rescncf  25124  ovoliunlem2  25730  voliun  25781  mbflimsup  25893  itgcn  26072  dvdsq1p  26388  aalioulem2  26564  recosf1o  26768  logrec  26996  xrlimcnp  27201  basellem4  27316  bposlem1  27516  bposlem5  27520  lgsqrmod  27584  lgsdchrval  27586  2lgslem1a1  27621  pntlem3  27841  nosupbnd1  27946  noinfbnd1  27961  oldbday  28162  lrcut  28165  abslts  28510  n0ssoldg  28614  zsoring  28670  bdayfinbndlem1  28728  isplng  29131  brbtwn2  29346  axbtwnid  29380  elntg2  29426  umgredgprv  29548  umgrpredgv  29581  usgredgprvALT  29639  fusgrfisstep  29773  fusgrfis  29774  nbupgr  29788  nbumgrvtx  29790  finsumvtxdg2size  29994  wlkp1lem8  30122  upgr2pthnlp  30181  wwlksnextinj  30351  usgr2wspthons3  30419  clwwlkccatlem  30443  clwlkclwwlklem2a1  30446  clwwisshclwws  30469  wwlksext2clwwlk  30511  clwwlknonex2lem2  30562  eucrctshift  30707  eucrct2eupth  30709  numclwwlk2lem1  30840  numclwwlk5lem  30851  frgrreggt1  30857  frgrreg  30858  friendship  30863  blocn2  31273  htthlem  31382  axhcompl-zf  31463  spanuni  32009  spansncol  32033  spansneleq  32035  elspansn5  32039  idcnop  32446  pjnormssi  32633  dmdmd  32765  n0nsnel  32974  ifeqeqx  33001  opabssi  33071  ac6mapd  33081  ressupprn  33147  supxrnemnf  33224  rexdiv  33356  xrstos  33435  cnre2csqlem  34405  fsumcvg4  34445  lmxrge0  34447  qqhval2lem  34476  esumpr2  34562  esumcvg  34581  issgon  34618  measxun2  34706  measres  34718  measdivcst  34720  measdivcstALTV  34721  elorrvc  34960  signsply0  35044  bnj580  35407  fnfvintima  35576  nummin  35583  axprALT2  35602  kardfi  35681  umgracycusgr  35718  erdsze2lem2  35768  cvmsval  35830  fmlasuc  35950  fundmpss  36331  dfon2lem3  36347  dfrdg4  36515  cgrtriv  36567  btwntriv2  36577  ifscgr  36609  lineext  36641  btwnconn1lem12  36663  colinbtwnle  36683  elicc3  36921  ontgval  37035  onsucconni  37041  axtco1from2  37079  axtcond  37082  axnulregtco  37084  dfttc4lem2  37133  bj-bibibi  37272  bj-cbvalvv  37354  bj-cbval  37361  bj-cbvex  37362  bj-cbvexw  37392  bj-nnf-cbval  37498  bj-equsal  37554  bj-gabeqd  37666  bj-restn0  37825  bj-snmoore  37848  cgsex2gd  37874  bj-elsn0  37892  bj-finsumval0  38022  relowlssretop  38102  sucneqond  38104  finxpsuc  38137  pibt2  38156  wl-nfs1t  38285  finixpnum  38344  ltflcei  38347  poimirlem23  38377  poimirlem24  38378  poimirlem27  38381  poimirlem32  38386  itg2addnclem  38405  areacirclem2  38443  areacirclem5  38446  areacirc  38447  nninfnub  38486  prdstotbnd  38529  heiborlem4  38549  heibor  38556  elghomlem2OLD  38621  grpokerinj  38628  isidlc  38750  disjlem17  39635  prtlem17  39734  dral1-o  39762  axc16g-o  39792  lsator0sp  39859  atlrelat1  40179  cvratlem  40279  diaintclN  41916  dibintclN  42025  cdlemn11pre  42068  dihord2pre  42083  dihintcl  42202  dochkrshp4  42247  lcfrlem9  42408  lcfrlem21  42421  mapdh8e  42642  aks4d1p5  42931  aks6d1c1p1  42958  sticksstones4  43000  0prjspnrel  43458  elrfirn2  43526  rencldnfilem  43646  onsupnmax  44054  onov0suclim  44100  oege1  44132  cantnfresb  44150  dflim5  44155  omabs2  44158  refimssco  44432  rtrclex  44442  intimasn  44482  ss2iundf  44484  ov2ssiunov2  44525  comptiunov2i  44531  iunrelexpuztr  44544  dssmapf1od  44846  mnringmulrcld  45051  mnuprdlem1  45081  mnuprdlem2  45082  snelpwrVD  45638  en3lplem1VD  45650  en3lpVD  45652  orbi1rVD  45655  sbc3orgVD  45658  3impexpVD  45663  equncomVD  45675  trsbcVD  45684  trintALTVD  45687  trintALT  45688  csbingVD  45691  csbsngVD  45700  csbxpgVD  45701  csbrngVD  45703  csbfv12gALTVD  45706  relopabVD  45708  e2ebindVD  45719  xlimpnfxnegmnf  46627  xlimbr  46640  stoweidlem35  46848  stoweidlem48  46861  ormkglobd  47690  n0nsn2el  47898  rexrsb  47973  2reu8i  47986  funbrafv  48031  rlimdmafv  48050  tz6.12c-afv2  48115  rlimdmafv2  48131  fzopredsuc  48197  2ffzoeq  48201  m1modnep2mod  48231  2timesltsq  48251  eqfvelsetpreimafv  48278  iccpartlt  48309  proththd  48502  even3prm2  48620  fppr2odd  48632  sbgoldbm  48685  nnsum3primesle9  48695  wtgoldbnnsum4prm  48703  bgoldbnnsum3prm  48705  grtrif1o  48843  mgm2mgm  49127  2zrngnmlid  49155  2zrngnmrid  49156  ellcoellss  49350  nneop  49441  fldivexpfllog2  49480  digexp  49522  reorelicc  49625  2itscp  49696  oppc1stflem  50198  prsthinc  50375  elpglem2  50623