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  1865  speivw  2005  spfw  2065  cbvalw  2067  alcomimw  2075  cbvalv1  2370  cbval  2427  axc16i  2465  sb3  2506  sb2  2508  axc16gALT  2519  ralbida  3273  rspcimdv  3566  rspcedv  3569  moi2  3673  moi  3675  sspsstr  4036  2nreu  4401  rabsnifsb  4682  ralxfr2d  5371  sbcop1  5457  isso2i  5595  wefrc  5644  elinxp  6007  sotri3  6123  oneqmini  6416  ordsssuc2  6456  ordtri2or  6463  iotan0  6528  2elresin  6660  f1ocnv  6837  fveqres  6929  fvun1  6976  dffo4  7103  funopsnOLD  7152  fconst5  7212  fnprb  7214  fntpb  7215  isores3  7343  f1oweOLD  7362  weniso  7364  ndmovordi  7612  abnexg  7770  ordsuc  7825  orduniorsuc  7841  ordzsl  7856  tfinds  7871  dmfexALT  7920  f1oweALT  7984  opreuopreu  8046  fnse  8150  poxp3  8167  poseq  8175  soseq  8176  tposfo2  8266  fprlem1  8318  issmo2  8357  iordsmo  8365  smoel2  8371  tz7.48lemOLD  8451  oawordeulem  8562  om00  8583  omlimcl  8586  odi  8587  nnawordi  8630  unfi  9186  php2  9223  fiint  9318  fipreima  9347  dffi2  9415  suplub2  9453  wemapsolem  9544  unwdomg  9578  inf3lem3  9631  wemapwe  9698  trcl  9729  frrlem15  9761  fidomtri  10074  prdom2  10085  cardaleph  10168  ackbij1lem16  10312  coflim  10339  coftr  10351  infpssrlem4  10384  isfin7-2  10474  axdc3lem2  10529  axdc3lem4  10531  brdom6disj  10611  entric  10641  fpwwe2lem11  10726  inatsk  10863  grur1a  10904  indpi  10992  reclem3pr  11134  supsrlem  11196  lelttr  11400  dedekindle  11474  negn0  11745  fimaxre  12261  fiminre  12264  nnmulcl  12359  arch  12603  nnnegz  12696  zle0orge1  12710  0nn0m1nnn0  12753  zeo  12785  uzm1  12999  rpneg  13154  xrlttri  13268  xrlelttr  13285  iccid  13521  icoshft  13604  fzen  13674  elfz1b  13727  fzdif1  13739  elfz2nn0  13752  fzoopth  13897  fleqceilz  13994  zmodidfzoimp  14041  modsumfzodifsn  14087  hasheqf1oi  14495  hashnfinnn0  14505  hashle2prv  14623  swrd0  14808  pfxccatin12lem2  14880  swrdccat  14884  swrdccat3blem  14888  repswswrd  14935  trclublem  15148  max0add  15477  abslt  15482  absle  15483  rexuzre  15520  caurcvg  15844  caucvg  15846  dvdsval2  16425  negdvdsb  16442  muldvds2  16451  dvdsabseq  16483  smuval2  16652  smupvallem  16653  rplpwr  16732  alginv  16750  algfx  16755  coprmgcdb  16824  divgcdcoprm0  16840  oddprmgt2  16875  rpexp1i  16899  qnumdencl  16915  phiprmpw  16953  prmdiveq  16963  prm23lt5  16992  pcmpt  17070  infpnlem1  17088  prmgaplem3  17231  prmgaplem8  17236  imasaddfnlem  17700  plelttr  18516  lubval  18528  lublecllem  18532  glbval  18541  mndind  19024  mndodconglem  19755  sdrgacs  21058  xrge0omnd  21751  elfrlmbasn0  22069  mavmulsolcl  22866  matunitlindflem1  22994  slesolex  23000  fvmptnn04if  23167  chfacfisf  23172  chfacfisfcpmat  23173  cnpnei  23582  unconn  23747  comppfsc  23851  kqsat  24050  isr0  24056  qtophmeo  24136  trufil  24229  alexsubALT  24370  cnextcn  24386  ucnima  24599  iducn  24601  bl2in  24719  addcnlem  25184  rescncf  25218  ovoliunlem2  25824  voliun  25875  mbflimsup  25987  itgcn  26165  dvdsq1p  26481  preimaaa  26646  aalioulem2  26660  recosf1o  26863  logrec  27091  xrlimcnp  27296  basellem4  27411  bposlem1  27611  bposlem5  27615  lgsqrmod  27679  lgsdchrval  27681  2lgslem1a1  27716  pntlem3  27936  nosupbnd1  28071  noinfbnd1  28086  oldbday  28287  lrcut  28290  abslts  28635  n0ssoldg  28739  zsoring  28795  bdayfinbndlem1  28853  isplng  29256  brbtwn2  29483  axbtwnid  29517  elntg2  29563  umgredgprv  29685  umgrpredgv  29718  usgredgprvALT  29776  fusgrfisstep  29910  fusgrfis  29911  nbupgr  29925  nbumgrvtx  29927  finsumvtxdg2size  30131  wlkp1lem8  30259  upgr2pthnlp  30318  wwlksnextinj  30488  usgr2wspthons3  30556  clwwlkccatlem  30580  clwlkclwwlklem2a1  30583  clwwisshclwws  30606  wwlksext2clwwlk  30648  clwwlknonex2lem2  30699  eucrctshift  30844  eucrct2eupth  30846  numclwwlk2lem1  30977  numclwwlk5lem  30988  frgrreggt1  30994  frgrreg  30995  friendship  31000  blocn2  31410  htthlem  31519  axhcompl-zf  31600  spanuni  32146  spansncol  32170  spansneleq  32172  elspansn5  32176  idcnop  32583  pjnormssi  32770  dmdmd  32902  n0nsnel  33111  ifeqeqx  33138  opabssi  33207  ac6mapd  33217  ressupprn  33283  supxrnemnf  33360  rexdiv  33492  xrstos  33571  cnre2csqlem  34542  fsumcvg4  34582  lmxrge0  34584  qqhval2lem  34613  esumpr2  34699  esumcvg  34718  issgon  34755  measxun2  34843  measres  34855  measdivcst  34857  measdivcstALTV  34858  elorrvc  35096  signsply0  35180  bnj580  35543  fnfvintima  35714  nummin  35722  axprALT2  35734  kardfi  35838  onprcf1acwevdlem1  35895  umgracycusgr  35919  erdsze2lem2  35969  cvmsval  36031  fmlasuc  36151  fundmpss  36532  dfon2lem3  36547  dfrdg4  36715  cgrtriv  36767  btwntriv2  36777  ifscgr  36809  lineext  36841  btwnconn1lem12  36863  colinbtwnle  36883  elicc3  37105  ontgval  37219  onsucconni  37225  axtco1from2  37263  axtcond  37266  axnulregtco  37268  dfttc4lem2  37317  bj-bibibi  37456  bj-cbvalvv  37538  bj-cbval  37545  bj-cbvex  37546  bj-cbvexw  37576  bj-nnf-cbval  37682  bj-equsal  37738  bj-gabeqd  37850  bj-restn0  38011  bj-snmoore  38034  cgsex2gd  38059  bj-elsn0  38077  bj-finsumval0  38207  relowlssretop  38287  sucneqond  38289  finxpsuc  38322  pibt2  38341  wl-nfs1t  38470  finixpnum  38529  ltflcei  38532  poimirlem23  38562  poimirlem24  38563  poimirlem27  38566  poimirlem32  38571  itg2addnclem  38590  areacirclem2  38628  areacirclem5  38631  areacirc  38632  nninfnub  38686  prdstotbnd  38729  heiborlem4  38749  heibor  38756  elghomlem2OLD  38821  grpokerinj  38828  isidlc  38950  disjlem17  39835  prtlem17  39934  dral1-o  39962  axc16g-o  39992  lsator0sp  40059  atlrelat1  40379  cvratlem  40479  diaintclN  42116  dibintclN  42225  cdlemn11pre  42268  dihord2pre  42283  dihintcl  42402  dochkrshp4  42447  lcfrlem9  42608  lcfrlem21  42621  mapdh8e  42842  aks4d1p5  43131  aks6d1c1p1  43158  sticksstones4  43200  0prjspnrel  43664  elrfirn2  43707  rencldnfilem  43827  onsupnmax  44230  onov0suclim  44276  oege1  44308  cantnfresb  44326  dflim5  44331  omabs2  44334  refimssco  44607  rtrclex  44617  intimasn  44657  ss2iundf  44659  ov2ssiunov2  44700  comptiunov2i  44706  iunrelexpuztr  44719  dssmapf1od  45021  mnringmulrcld  45226  mnuprdlem1  45256  mnuprdlem2  45257  snelpwrVD  45813  en3lplem1VD  45825  en3lpVD  45827  orbi1rVD  45830  sbc3orgVD  45833  3impexpVD  45838  equncomVD  45850  trsbcVD  45859  trintALTVD  45862  trintALT  45863  csbingVD  45866  csbsngVD  45875  csbxpgVD  45876  csbrngVD  45878  csbfv12gALTVD  45881  relopabVD  45883  e2ebindVD  45894  cocanss2  45922  xlimpnfxnegmnf  46824  xlimbr  46837  stoweidlem35  47045  stoweidlem48  47058  ormkglobd  47887  n0nsn2el  48095  rexrsb  48170  2reu8i  48183  funbrafv  48228  rlimdmafv  48247  tz6.12c-afv2  48312  rlimdmafv2  48328  fzopredsuc  48394  2ffzoeq  48398  m1modnep2mod  48428  2timesltsq  48448  eqfvelsetpreimafv  48475  iccpartlt  48506  proththd  48699  even3prm2  48817  fppr2odd  48829  sbgoldbm  48882  nnsum3primesle9  48892  wtgoldbnnsum4prm  48900  bgoldbnnsum3prm  48902  grtrif1o  49040  mgm2mgm  49324  2zrngnmlid  49352  2zrngnmrid  49353  ellcoellss  49547  nneop  49638  fldivexpfllog2  49677  digexp  49719  reorelicc  49822  2itscp  49893  oppc1stflem  50395  prsthinc  50572  elpglem2  50805