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  2008  spfw  2068  cbvalw  2070  alcomimw  2078  cbvalv1  2374  cbval  2430  axc16i  2468  sb3  2509  sb2  2511  axc16gALT  2522  ralbida  3277  rspcimdv  3570  rspcedv  3573  moi2  3677  moi  3679  sspsstr  4039  2nreu  4405  rabsnifsb  4683  ralxfr2d  5376  sbcop1  5462  isso2i  5600  wefrc  5649  elinxp  6019  sotri3  6135  oneqmini  6431  ordsssuc2  6471  ordtri2or  6478  iotan0  6544  iotan0OLD  6545  2elresin  6679  f1ocnv  6856  fveqres  6949  fvun1  6996  dffo4  7124  funopsnOLD  7173  fconst5  7232  fnprb  7234  fntpb  7235  isores3  7363  f1oweOLD  7382  weniso  7384  ndmovordi  7633  abnexg  7791  ordsuc  7846  orduniorsuc  7862  ordzsl  7877  tfinds  7892  dmfexALT  7941  f1oweALT  8005  opreuopreu  8067  ovmptss  8126  fnse  8174  poxp3  8191  poseq  8199  soseq  8200  tposfo2  8291  fprlem1  8343  issmo2  8382  iordsmo  8390  smoel2  8396  tz7.48lemOLD  8476  oawordeulem  8587  om00  8608  omlimcl  8611  odi  8612  nnawordi  8655  unfi  9211  php2  9248  fiint  9343  fipreima  9372  dffi2  9439  suplub2  9477  wemapsolem  9568  unwdomg  9602  inf3lem3  9655  wemapwe  9722  trcl  9753  frrlem15  9785  fidomtri  10098  prdom2  10109  cardaleph  10192  ackbij1lem16  10336  coflim  10363  coftr  10375  infpssrlem4  10408  isfin7-2  10498  axdc3lem2  10553  axdc3lem4  10555  brdom6disj  10635  entric  10665  fpwwe2lem11  10750  inatsk  10887  grur1a  10928  indpi  11016  reclem3pr  11158  supsrlem  11220  lelttr  11424  dedekindle  11498  negn0  11769  fimaxre  12285  fiminre  12288  nnmulcl  12383  arch  12627  nnnegz  12720  zle0orge1  12734  0nn0m1nnn0  12777  zeo  12809  uzm1  13023  rpneg  13178  xrlttri  13292  xrlelttr  13309  iccid  13545  icoshft  13628  fzen  13698  elfz1b  13751  fzdif1  13763  elfz2nn0  13776  fzoopth  13921  fleqceilz  14018  zmodidfzoimp  14065  modsumfzodifsn  14111  hasheqf1oi  14519  hashnfinnn0  14529  hashle2prv  14647  swrd0  14833  pfxccatin12lem2  14905  swrdccat  14909  swrdccat3blem  14913  repswswrd  14960  trclublem  15174  max0add  15503  abslt  15508  absle  15509  rexuzre  15546  caurcvg  15870  caucvg  15872  dvdsval2  16451  negdvdsb  16468  muldvds2  16477  dvdsabseq  16509  smuval2  16678  smupvallem  16679  rplpwr  16758  alginv  16776  algfx  16781  coprmgcdb  16850  divgcdcoprm0  16866  oddprmgt2  16901  rpexp1i  16925  qnumdencl  16941  phiprmpw  16979  prmdiveq  16989  prm23lt5  17018  pcmpt  17096  infpnlem1  17114  prmgaplem3  17257  prmgaplem8  17262  imasaddfnlem  17726  plelttr  18542  lubval  18554  lublecllem  18558  glbval  18567  mndind  19050  mndodconglem  19782  sdrgacs  21085  xrge0omnd  21778  elfrlmbasn0  22096  mavmulsolcl  22893  matunitlindflem1  23021  slesolex  23027  fvmptnn04if  23194  chfacfisf  23199  chfacfisfcpmat  23200  cnpnei  23609  unconn  23774  comppfsc  23878  kqsat  24077  isr0  24083  qtophmeo  24163  trufil  24256  alexsubALT  24397  cnextcn  24413  ucnima  24626  iducn  24628  bl2in  24746  addcnlem  25211  rescncf  25245  ovoliunlem2  25851  voliun  25902  mbflimsup  26014  itgcn  26192  dvdsq1p  26508  preimaaa  26673  aalioulem2  26687  recosf1o  26890  logrec  27118  xrlimcnp  27323  basellem4  27438  bposlem1  27638  bposlem5  27642  lgsqrmod  27706  lgsdchrval  27708  2lgslem1a1  27743  pntlem3  27963  nosupbnd1  28098  noinfbnd1  28113  oldbday  28314  lrcut  28317  abslts  28662  n0ssoldg  28766  zsoring  28822  bdayfinbndlem1  28880  isplng  29283  brbtwn2  29510  axbtwnid  29544  elntg2  29590  umgredgprv  29712  umgrpredgv  29745  usgredgprvALT  29803  fusgrfisstep  29937  fusgrfis  29938  nbupgr  29952  nbumgrvtx  29954  finsumvtxdg2size  30158  wlkp1lem8  30286  upgr2pthnlp  30345  wwlksnextinj  30515  usgr2wspthons3  30583  clwwlkccatlem  30607  clwlkclwwlklem2a1  30610  clwwisshclwws  30633  wwlksext2clwwlk  30675  clwwlknonex2lem2  30726  eucrctshift  30871  eucrct2eupth  30873  numclwwlk2lem1  31004  numclwwlk5lem  31015  frgrreggt1  31021  frgrreg  31022  friendship  31027  blocn2  31437  htthlem  31546  axhcompl-zf  31627  spanuni  32173  spansncol  32197  spansneleq  32199  elspansn5  32203  idcnop  32610  pjnormssi  32797  dmdmd  32929  n0nsnel  33180  ifeqeqx  33207  opabssi  33276  ac6mapd  33286  ressupprn  33351  supxrnemnf  33427  rexdiv  33559  xrstos  33638  cnre2csqlem  34609  fsumcvg4  34649  lmxrge0  34651  qqhval2lem  34680  esumpr2  34766  esumcvg  34785  issgon  34822  measxun2  34910  measres  34922  measdivcst  34924  measdivcstALTV  34925  elorrvc  35163  signsply0  35247  bnj580  35610  fnfvintima  35783  nummin  35803  axprALT2  35815  kardfi  35937  dfk12  36011  dfk22  36012  dfk32  36013  onprcf1acwevdlem1  36044  umgracycusgr  36075  srepdflem1  36084  erdsze2lem2  36135  cvmsval  36197  fmlasuc  36317  mirimanoffr  36626  fundmpss  36709  dfon2lem3  36724  dfrdg4  36892  cgrtriv  36944  btwntriv2  36954  ifscgr  36986  lineext  37018  btwnconn1lem12  37040  colinbtwnle  37060  elicc3  37282  ontgval  37396  onsucconni  37402  axtco1from2  37440  axtcond  37443  axnulregtco  37445  dfttc4lem2  37494  bj-bibibi  37633  bj-cbvalvv  37715  bj-cbval  37722  bj-cbvex  37723  bj-cbvexw  37753  bj-nnf-cbval  37859  bj-equsal  37915  bj-gabeqd  38027  bj-restn0  38201  bj-snmoore  38224  cgsex2gd  38249  bj-elsn0  38267  bj-finsumval0  38397  relowlssretop  38477  sucneqond  38479  finxpsuc  38512  pibt2  38531  wl-nfs1t  38660  finixpnum  38719  ltflcei  38722  poimirlem23  38752  poimirlem24  38753  poimirlem27  38756  poimirlem32  38761  itg2addnclem  38780  areacirclem2  38818  areacirclem5  38821  areacirc  38822  nninfnub  38876  prdstotbnd  38919  heiborlem4  38939  heibor  38946  elghomlem2OLD  39011  grpokerinj  39018  isidlc  39140  disjlem17  40025  prtlem17  40124  dral1-o  40152  axc16g-o  40182  lsator0sp  40249  atlrelat1  40569  cvratlem  40669  diaintclN  42306  dibintclN  42415  cdlemn11pre  42458  dihord2pre  42473  dihintcl  42592  dochkrshp4  42637  lcfrlem9  42798  lcfrlem21  42811  mapdh8e  43032  aks4d1p5  43321  aks6d1c1p1  43348  sticksstones4  43390  0prjspnrel  43854  elrfirn2  43898  rencldnfilem  44018  onsupnmax  44420  onov0suclim  44466  oege1  44498  cantnfresb  44516  dflim5  44521  omabs2  44524  refimssco  44797  rtrclex  44807  intimasn  44847  ss2iundf  44849  ov2ssiunov2  44890  comptiunov2i  44896  iunrelexpuztr  44909  dssmapf1od  45211  mnringmulrcld  45416  mnuprdlem1  45446  mnuprdlem2  45447  snelpwrVD  46002  en3lplem1VD  46014  en3lpVD  46016  orbi1rVD  46019  sbc3orgVD  46022  3impexpVD  46027  equncomVD  46039  trsbcVD  46048  trintALTVD  46051  trintALT  46052  csbingVD  46055  csbsngVD  46064  csbxpgVD  46065  csbrngVD  46067  csbfv12gALTVD  46070  relopabVD  46072  e2ebindVD  46083  cocanss2  46112  xlimpnfxnegmnf  47027  xlimbr  47040  stoweidlem35  47248  stoweidlem48  47261  ormkglobd  48090  n0nsn2el  48298  aiotaexim  48371  rexrsb  48374  2reu8i  48387  funbrafv  48431  rlimdmafv  48450  tz6.12c-afv2  48515  rlimdmafv2  48531  fzopredsuc  48597  2ffzoeq  48601  m1modnep2mod  48631  2timesltsq  48651  eqfvelsetpreimafv  48678  iccpartlt  48709  proththd  48902  even3prm2  49020  fppr2odd  49032  sbgoldbm  49085  nnsum3primesle9  49095  wtgoldbnnsum4prm  49103  bgoldbnnsum3prm  49105  grtrif1o  49243  mgm2mgm  49527  2zrngnmlid  49555  2zrngnmrid  49556  ellcoellss  49750  nneop  49841  fldivexpfllog2  49880  digexp  49922  reorelicc  50025  2itscp  50096  oppc1stflem  50612  prsthinc  50802  elpglem2  51083