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  ralbida  3249  rspcimdv  3555  rspcedv  3558  moi2  3663  moi  3665  sspsstr  4049  2nreu  4385  rabsnifsb  4667  ralxfr2d  5349  axprlem4OLD  5369  sbcop1  5438  isso2i  5571  wefrc  5620  elinxp  5980  sotri3  6089  oneqmini  6372  ordsssuc2  6412  ordtri2or  6419  iotan0  6484  2elresin  6615  f1ocnv  6788  fveqres  6880  fvun1  6927  dffo4  7051  funopsn  7097  fconst5  7156  fnprb  7158  fntpb  7159  isores3  7285  f1owe  7303  weniso  7304  ndmovordi  7553  abnexg  7705  ordsuc  7760  orduniorsuc  7776  ordzsl  7791  tfinds  7806  dmfexALT  7854  f1oweALT  7920  opreuopreu  7982  fnse  8078  poxp3  8095  poseq  8103  soseq  8104  tposfo2  8194  fprlem1  8245  issmo2  8284  iordsmo  8292  smoel2  8298  tz7.48lem  8375  oawordeulem  8484  om00  8505  omlimcl  8508  odi  8509  nnawordi  8552  unfi  9100  php2  9137  fiint  9232  fipreima  9263  dffi2  9331  suplub2  9369  wemapsolem  9460  unwdomg  9494  inf3lem3  9546  trcl  9644  frrlem15  9676  fidomtri  9912  prdom2  9923  cardaleph  10006  ackbij1lem16  10151  coflim  10178  coftr  10190  infpssrlem4  10223  isfin7-2  10313  axdc3lem2  10368  axdc3lem4  10370  brdom6disj  10449  entric  10474  fpwwe2lem11  10559  inatsk  10696  grur1a  10737  indpi  10825  reclem3pr  10967  supsrlem  11029  lelttr  11231  dedekindle  11305  negn0  11574  fimaxre  12095  fiminre  12098  nnmulcl  12193  arch  12429  nnnegz  12522  zle0orge1  12536  zeo  12610  uzm1  12817  rpneg  12971  xrlttri  13085  xrlelttr  13102  iccid  13338  icoshft  13421  fzen  13490  elfz1b  13542  fzdif1  13554  elfz2nn0  13567  fzoopth  13712  fleqceilz  13808  zmodidfzoimp  13855  modsumfzodifsn  13901  hasheqf1oi  14308  hashnfinnn0  14318  hashle2prv  14435  swrd0  14616  pfxccatin12lem2  14688  swrdccat  14692  swrdccat3blem  14696  repswswrd  14741  trclublem  14952  max0add  15267  abslt  15272  absle  15273  rexuzre  15310  caurcvg  15634  caucvg  15636  dvdsval2  16219  negdvdsb  16236  muldvds2  16245  dvdsabseq  16277  smuval2  16446  smupvallem  16447  rplpwr  16522  alginv  16539  algfx  16544  coprmgcdb  16613  divgcdcoprm0  16629  oddprmgt2  16664  rpexp1i  16688  qnumdencl  16704  phiprmpw  16741  prmdiveq  16751  prm23lt5  16780  pcmpt  16858  infpnlem1  16876  prmgaplem3  17019  prmgaplem8  17024  imasaddfnlem  17487  plelttr  18303  lubval  18315  lublecllem  18319  glbval  18328  mndind  18791  mndodconglem  19511  sdrgacs  20773  xrge0omnd  21439  elfrlmbasn0  21757  mavmulsolcl  22530  slesolex  22661  fvmptnn04if  22828  chfacfisf  22833  chfacfisfcpmat  22834  cnpnei  23243  unconn  23408  comppfsc  23511  kqsat  23710  isr0  23716  qtophmeo  23796  trufil  23889  alexsubALT  24030  cnextcn  24046  ucnima  24259  iducn  24261  bl2in  24379  addcnlem  24844  rescncf  24878  ovoliunlem2  25484  voliun  25535  mbflimsup  25647  itgcn  25826  dvdsq1p  26142  aalioulem2  26314  recosf1o  26516  logrec  26744  xrlimcnp  26949  basellem4  27065  bposlem1  27265  bposlem5  27269  lgsqrmod  27333  lgsdchrval  27335  2lgslem1a1  27370  pntlem3  27590  nosupbnd1  27696  noinfbnd1  27711  oldbday  27911  lrcut  27914  abslts  28259  n0ssoldg  28363  zsoring  28419  bdayfinbndlem1  28477  brbtwn2  28992  axbtwnid  29026  elntg2  29072  umgredgprv  29194  umgrpredgv  29227  usgredgprvALT  29282  fusgrfisstep  29416  fusgrfis  29417  nbupgr  29431  nbumgrvtx  29433  finsumvtxdg2size  29638  wlkp1lem8  29766  upgr2pthnlp  29819  wwlksnextinj  29986  usgr2wspthons3  30054  clwwlkccatlem  30078  clwlkclwwlklem2a1  30081  clwwisshclwws  30104  wwlksext2clwwlk  30146  clwwlknonex2lem2  30197  eucrctshift  30332  eucrct2eupth  30334  numclwwlk2lem1  30465  numclwwlk5lem  30476  frgrreggt1  30482  frgrreg  30483  friendship  30488  blocn2  30898  htthlem  31007  axhcompl-zf  31088  spanuni  31634  spansncol  31658  spansneleq  31660  elspansn5  31664  idcnop  32071  pjnormssi  32258  dmdmd  32390  bian1dOLD  32545  n0nsnel  32604  ifeqeqx  32631  opabssi  32705  ac6mapd  32715  ressupprn  32782  supxrnemnf  32860  rexdiv  33004  xrstos  33089  cnre2csqlem  34074  fsumcvg4  34114  lmxrge0  34116  qqhval2lem  34145  esumpr2  34231  esumcvg  34250  issgon  34287  measxun2  34374  measres  34386  measdivcst  34388  measdivcstALTV  34389  elorrvc  34628  signsply0  34715  bnj580  35075  nummin  35256  axprALT2  35273  0nn0m1nnn0  35315  umgracycusgr  35356  erdsze2lem2  35406  cvmsval  35468  fmlasuc  35588  fundmpss  35969  dfon2lem3  35985  dfrdg4  36153  cgrtriv  36204  btwntriv2  36214  ifscgr  36246  lineext  36278  btwnconn1lem12  36300  colinbtwnle  36320  elicc3  36519  ontgval  36633  onsucconni  36639  axtco1from2  36677  axtcond  36680  axnulregtco  36682  dfttc4lem2  36731  bj-bibibi  36871  bj-cbvalvv  36953  bj-cbval  36960  bj-cbvex  36961  bj-cbvexw  36991  bj-nnf-cbval  37097  bj-equsal  37153  bj-gabeqd  37264  bj-restn0  37422  bj-snmoore  37445  cgsex2gd  37471  bj-elsn0  37489  bj-finsumval0  37619  relowlssretop  37697  sucneqond  37699  finxpsuc  37732  pibt2  37751  wl-nfs1t  37880  finixpnum  37944  ltflcei  37947  matunitlindflem1  37955  poimirlem23  37982  poimirlem24  37983  poimirlem27  37986  poimirlem32  37991  itg2addnclem  38010  areacirclem2  38048  areacirclem5  38051  areacirc  38052  nninfnub  38090  prdstotbnd  38133  heiborlem4  38153  heibor  38160  elghomlem2OLD  38225  grpokerinj  38232  isidlc  38354  disjlem17  39241  prtlem17  39340  dral1-o  39368  axc16g-o  39398  lsator0sp  39465  atlrelat1  39785  cvratlem  39885  diaintclN  41522  dibintclN  41631  cdlemn11pre  41674  dihord2pre  41689  dihintcl  41808  dochkrshp4  41853  lcfrlem9  42014  lcfrlem21  42027  mapdh8e  42248  aks4d1p5  42537  aks6d1c1p1  42564  sticksstones4  42606  0prjspnrel  43078  elrfirn2  43146  rencldnfilem  43270  onsupnmax  43678  onov0suclim  43724  oege1  43756  cantnfresb  43774  dflim5  43779  omabs2  43782  refimssco  44056  rtrclex  44066  intimasn  44106  ss2iundf  44108  ov2ssiunov2  44149  comptiunov2i  44155  iunrelexpuztr  44168  dssmapf1od  44470  mnringmulrcld  44677  mnuprdlem1  44721  mnuprdlem2  44722  snelpwrVD  45279  en3lplem1VD  45291  en3lpVD  45293  orbi1rVD  45296  sbc3orgVD  45299  3impexpVD  45304  equncomVD  45316  trsbcVD  45325  trintALTVD  45328  trintALT  45329  csbingVD  45332  csbsngVD  45341  csbxpgVD  45342  csbrngVD  45344  csbfv12gALTVD  45347  relopabVD  45349  e2ebindVD  45360  xlimpnfxnegmnf  46264  xlimbr  46277  stoweidlem35  46485  stoweidlem48  46498  ormkglobd  47325  cjnpoly  47353  tannpoly  47354  n0nsn2el  47489  rexrsb  47564  2reu8i  47577  funbrafv  47622  rlimdmafv  47641  tz6.12c-afv2  47706  rlimdmafv2  47722  fzopredsuc  47788  2ffzoeq  47792  m1modnep2mod  47822  2timesltsq  47842  eqfvelsetpreimafv  47869  iccpartlt  47900  proththd  48093  even3prm2  48211  fppr2odd  48223  sbgoldbm  48276  nnsum3primesle9  48286  wtgoldbnnsum4prm  48294  bgoldbnnsum3prm  48296  grtrif1o  48434  mgm2mgm  48719  2zrngnmlid  48747  2zrngnmrid  48748  ellcoellss  48927  nneop  49018  fldivexpfllog2  49057  digexp  49099  reorelicc  49202  2itscp  49273  oppc1stflem  49778  prsthinc  49955  elpglem2  50203