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  1054  alexbii  1834  speivw  1974  spfw  2034  cbvalw  2036  alcomimw  2044  cbvalv1  2341  cbval  2398  axc16i  2436  sb3  2477  sb2  2479  axc16gALT  2490  eqrdav  2730  ralbida  3243  rspcimdv  3562  rspcedv  3565  moi2  3670  moi  3672  sspsstr  4055  2nreu  4391  rabsnifsb  4672  ralxfr2d  5346  axprlem4OLD  5365  sbcop1  5426  isso2i  5559  wefrc  5608  elinxp  5967  sotri3  6076  oneqmini  6359  ordsssuc2  6399  ordtri2or  6406  iotan0  6471  2elresin  6602  f1ocnv  6775  fveqres  6866  fvun1  6913  dffo4  7036  funopsn  7081  fconst5  7140  fnprb  7142  fntpb  7143  isores3  7269  f1owe  7287  weniso  7288  ndmovordi  7537  abnexg  7689  ordsuc  7744  orduniorsuc  7760  ordzsl  7775  tfinds  7790  dmfexALT  7838  f1oweALT  7904  opreuopreu  7966  fnse  8063  poxp3  8080  poseq  8088  soseq  8089  tposfo2  8179  fprlem1  8230  issmo2  8269  iordsmo  8277  smoel2  8283  tz7.48lem  8360  oawordeulem  8469  om00  8490  omlimcl  8493  odi  8494  nnawordi  8536  unfi  9080  php2  9117  fiint  9211  fipreima  9242  dffi2  9307  suplub2  9345  wemapsolem  9436  unwdomg  9470  inf3lem3  9520  trcl  9618  frrlem15  9650  fidomtri  9886  prdom2  9897  cardaleph  9980  ackbij1lem16  10125  coflim  10152  coftr  10164  infpssrlem4  10197  isfin7-2  10287  axdc3lem2  10342  axdc3lem4  10344  brdom6disj  10423  entric  10448  fpwwe2lem11  10532  inatsk  10669  grur1a  10710  indpi  10798  reclem3pr  10940  supsrlem  11002  lelttr  11203  dedekindle  11277  negn0  11546  fimaxre  12066  fiminre  12069  nnmulcl  12149  arch  12378  nnnegz  12471  zle0orge1  12485  zeo  12559  uzm1  12770  rpneg  12924  xrlttri  13038  xrlelttr  13055  iccid  13290  icoshft  13373  fzen  13441  elfz1b  13493  fzdif1  13505  elfz2nn0  13518  fzoopth  13662  fleqceilz  13758  zmodidfzoimp  13805  modsumfzodifsn  13851  hasheqf1oi  14258  hashnfinnn0  14268  hashle2prv  14385  swrd0  14566  pfxccatin12lem2  14638  swrdccat  14642  swrdccat3blem  14646  repswswrd  14691  trclublem  14902  max0add  15217  abslt  15222  absle  15223  rexuzre  15260  caurcvg  15584  caucvg  15586  dvdsval2  16166  negdvdsb  16183  muldvds2  16192  dvdsabseq  16224  smuval2  16393  smupvallem  16394  rplpwr  16469  alginv  16486  algfx  16491  coprmgcdb  16560  divgcdcoprm0  16576  oddprmgt2  16610  rpexp1i  16634  qnumdencl  16650  phiprmpw  16687  prmdiveq  16697  prm23lt5  16726  pcmpt  16804  infpnlem1  16822  prmgaplem3  16965  prmgaplem8  16970  imasaddfnlem  17432  plelttr  18248  lubval  18260  lublecllem  18264  glbval  18273  mndind  18736  mndodconglem  19453  sdrgacs  20716  xrge0omnd  21382  elfrlmbasn0  21700  mavmulsolcl  22466  slesolex  22597  fvmptnn04if  22764  chfacfisf  22769  chfacfisfcpmat  22770  cnpnei  23179  unconn  23344  comppfsc  23447  kqsat  23646  isr0  23652  qtophmeo  23732  trufil  23825  alexsubALT  23966  cnextcn  23982  ucnima  24195  iducn  24197  bl2in  24315  addcnlem  24780  rescncf  24817  ovoliunlem2  25431  voliun  25482  mbflimsup  25594  itgcn  25773  dvdsq1p  26095  aalioulem2  26268  recosf1o  26471  logrec  26700  xrlimcnp  26905  basellem4  27021  bposlem1  27222  bposlem5  27226  lgsqrmod  27290  lgsdchrval  27292  2lgslem1a1  27327  pntlem3  27547  nosupbnd1  27653  noinfbnd1  27668  oldbday  27846  lrcut  27849  absslt  28187  zsoring  28332  brbtwn2  28883  axbtwnid  28917  elntg2  28963  umgredgprv  29085  umgrpredgv  29118  usgredgprvALT  29173  fusgrfisstep  29307  fusgrfis  29308  nbupgr  29322  nbumgrvtx  29324  finsumvtxdg2size  29529  wlkp1lem8  29657  upgr2pthnlp  29710  wwlksnextinj  29877  usgr2wspthons3  29945  clwwlkccatlem  29969  clwlkclwwlklem2a1  29972  clwwisshclwws  29995  wwlksext2clwwlk  30037  clwwlknonex2lem2  30088  eucrctshift  30223  eucrct2eupth  30225  numclwwlk2lem1  30356  numclwwlk5lem  30367  frgrreggt1  30373  frgrreg  30374  friendship  30379  blocn2  30788  htthlem  30897  axhcompl-zf  30978  spanuni  31524  spansncol  31548  spansneleq  31550  elspansn5  31554  idcnop  31961  pjnormssi  32148  dmdmd  32280  bian1dOLD  32436  n0nsnel  32495  ifeqeqx  32522  opabssi  32596  ac6mapd  32606  ressupprn  32671  supxrnemnf  32751  rexdiv  32906  xrstos  32991  cnre2csqlem  33923  fsumcvg4  33963  lmxrge0  33965  qqhval2lem  33994  esumpr2  34080  esumcvg  34099  issgon  34136  measxun2  34223  measres  34235  measdivcst  34237  measdivcstALTV  34238  elorrvc  34477  signsply0  34564  bnj580  34925  nummin  35104  0nn0m1nnn0  35157  umgracycusgr  35198  erdsze2lem2  35248  cvmsval  35310  fmlasuc  35430  fundmpss  35811  dfon2lem3  35827  dfrdg4  35995  cgrtriv  36046  btwntriv2  36056  ifscgr  36088  lineext  36120  btwnconn1lem12  36142  colinbtwnle  36162  elicc3  36361  ontgval  36475  onsucconni  36481  bj-bibibi  36630  bj-cbval  36693  bj-cbvex  36694  bj-cbvexw  36720  bj-equsal  36870  bj-gabeqd  36981  bj-restn0  37134  bj-snmoore  37157  bj-elsn0  37199  bj-finsumval0  37329  relowlssretop  37407  sucneqond  37409  finxpsuc  37442  pibt2  37461  wl-nfs1t  37581  finixpnum  37644  ltflcei  37647  matunitlindflem1  37655  poimirlem23  37682  poimirlem24  37683  poimirlem27  37686  poimirlem32  37691  itg2addnclem  37710  areacirclem2  37748  areacirclem5  37751  areacirc  37752  nninfnub  37790  prdstotbnd  37833  heiborlem4  37853  heibor  37860  elghomlem2OLD  37925  grpokerinj  37932  isidlc  38054  disjlem17  38896  prtlem17  38974  dral1-o  39002  axc16g-o  39032  lsator0sp  39099  atlrelat1  39419  cvratlem  39519  diaintclN  41156  dibintclN  41265  cdlemn11pre  41308  dihord2pre  41323  dihintcl  41442  dochkrshp4  41487  lcfrlem9  41648  lcfrlem21  41661  mapdh8e  41882  aks4d1p5  42172  aks6d1c1p1  42199  sticksstones4  42241  0prjspnrel  42719  elrfirn2  42788  rencldnfilem  42912  onsupnmax  43320  onov0suclim  43366  oege1  43398  cantnfresb  43416  dflim5  43421  omabs2  43424  refimssco  43699  rtrclex  43709  intimasn  43749  ss2iundf  43751  ov2ssiunov2  43792  comptiunov2i  43798  iunrelexpuztr  43811  dssmapf1od  44113  mnringmulrcld  44320  mnuprdlem1  44364  mnuprdlem2  44365  snelpwrVD  44922  en3lplem1VD  44934  en3lpVD  44936  orbi1rVD  44939  sbc3orgVD  44942  3impexpVD  44947  equncomVD  44959  trsbcVD  44968  trintALTVD  44971  trintALT  44972  csbingVD  44975  csbsngVD  44984  csbxpgVD  44985  csbrngVD  44987  csbfv12gALTVD  44990  relopabVD  44992  e2ebindVD  45003  xlimpnfxnegmnf  45911  xlimbr  45924  stoweidlem35  46132  stoweidlem48  46145  ormkglobd  46972  cjnpoly  46988  tannpoly  46989  n0nsn2el  47124  rexrsb  47199  2reu8i  47212  funbrafv  47257  rlimdmafv  47276  tz6.12c-afv2  47341  rlimdmafv2  47357  fzopredsuc  47422  2ffzoeq  47426  m1modnep2mod  47451  eqfvelsetpreimafv  47492  iccpartlt  47523  proththd  47713  even3prm2  47818  fppr2odd  47830  sbgoldbm  47883  nnsum3primesle9  47893  wtgoldbnnsum4prm  47901  bgoldbnnsum3prm  47903  grtrif1o  48041  mgm2mgm  48326  2zrngnmlid  48354  2zrngnmrid  48355  ellcoellss  48535  nneop  48626  fldivexpfllog2  48665  digexp  48707  reorelicc  48810  2itscp  48881  oppc1stflem  49387  prsthinc  49564  elpglem2  49812