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  2345  cbval  2402  axc16i  2440  sb3  2481  sb2  2483  axc16gALT  2494  ralbida  3248  rspcimdv  3554  rspcedv  3557  moi2  3662  moi  3664  sspsstr  4048  2nreu  4384  rabsnifsb  4666  ralxfr2d  5352  axprlem4OLD  5372  sbcop1  5441  isso2i  5576  wefrc  5625  elinxp  5984  sotri3  6093  oneqmini  6376  ordsssuc2  6416  ordtri2or  6423  iotan0  6488  2elresin  6619  f1ocnv  6792  fveqres  6884  fvun1  6931  dffo4  7055  funopsnOLD  7102  fconst5  7161  fnprb  7163  fntpb  7164  isores3  7290  f1owe  7308  weniso  7309  ndmovordi  7558  abnexg  7710  ordsuc  7765  orduniorsuc  7781  ordzsl  7796  tfinds  7811  dmfexALT  7859  f1oweALT  7925  opreuopreu  7987  fnse  8083  poxp3  8100  poseq  8108  soseq  8109  tposfo2  8199  fprlem1  8250  issmo2  8289  iordsmo  8297  smoel2  8303  tz7.48lem  8380  oawordeulem  8489  om00  8510  omlimcl  8513  odi  8514  nnawordi  8557  unfi  9105  php2  9142  fiint  9237  fipreima  9268  dffi2  9336  suplub2  9374  wemapsolem  9465  unwdomg  9499  inf3lem3  9551  trcl  9649  frrlem15  9681  fidomtri  9917  prdom2  9928  cardaleph  10011  ackbij1lem16  10156  coflim  10183  coftr  10195  infpssrlem4  10228  isfin7-2  10318  axdc3lem2  10373  axdc3lem4  10375  brdom6disj  10454  entric  10479  fpwwe2lem11  10564  inatsk  10701  grur1a  10742  indpi  10830  reclem3pr  10972  supsrlem  11034  lelttr  11236  dedekindle  11310  negn0  11579  fimaxre  12100  fiminre  12103  nnmulcl  12198  arch  12434  nnnegz  12527  zle0orge1  12541  zeo  12615  uzm1  12822  rpneg  12976  xrlttri  13090  xrlelttr  13107  iccid  13343  icoshft  13426  fzen  13495  elfz1b  13547  fzdif1  13559  elfz2nn0  13572  fzoopth  13717  fleqceilz  13813  zmodidfzoimp  13860  modsumfzodifsn  13906  hasheqf1oi  14313  hashnfinnn0  14323  hashle2prv  14440  swrd0  14621  pfxccatin12lem2  14693  swrdccat  14697  swrdccat3blem  14701  repswswrd  14746  trclublem  14957  max0add  15272  abslt  15277  absle  15278  rexuzre  15315  caurcvg  15639  caucvg  15641  dvdsval2  16224  negdvdsb  16241  muldvds2  16250  dvdsabseq  16282  smuval2  16451  smupvallem  16452  rplpwr  16527  alginv  16544  algfx  16549  coprmgcdb  16618  divgcdcoprm0  16634  oddprmgt2  16669  rpexp1i  16693  qnumdencl  16709  phiprmpw  16746  prmdiveq  16756  prm23lt5  16785  pcmpt  16863  infpnlem1  16881  prmgaplem3  17024  prmgaplem8  17029  imasaddfnlem  17492  plelttr  18308  lubval  18320  lublecllem  18324  glbval  18333  mndind  18796  mndodconglem  19516  sdrgacs  20778  xrge0omnd  21425  elfrlmbasn0  21743  mavmulsolcl  22516  slesolex  22647  fvmptnn04if  22814  chfacfisf  22819  chfacfisfcpmat  22820  cnpnei  23229  unconn  23394  comppfsc  23497  kqsat  23696  isr0  23702  qtophmeo  23782  trufil  23875  alexsubALT  24016  cnextcn  24032  ucnima  24245  iducn  24247  bl2in  24365  addcnlem  24830  rescncf  24864  ovoliunlem2  25470  voliun  25521  mbflimsup  25633  itgcn  25812  dvdsq1p  26128  aalioulem2  26299  recosf1o  26499  logrec  26727  xrlimcnp  26932  basellem4  27047  bposlem1  27247  bposlem5  27251  lgsqrmod  27315  lgsdchrval  27317  2lgslem1a1  27352  pntlem3  27572  nosupbnd1  27678  noinfbnd1  27693  oldbday  27893  lrcut  27896  abslts  28241  n0ssoldg  28345  zsoring  28401  bdayfinbndlem1  28459  brbtwn2  28974  axbtwnid  29008  elntg2  29054  umgredgprv  29176  umgrpredgv  29209  usgredgprvALT  29264  fusgrfisstep  29398  fusgrfis  29399  nbupgr  29413  nbumgrvtx  29415  finsumvtxdg2size  29619  wlkp1lem8  29747  upgr2pthnlp  29800  wwlksnextinj  29967  usgr2wspthons3  30035  clwwlkccatlem  30059  clwlkclwwlklem2a1  30062  clwwisshclwws  30085  wwlksext2clwwlk  30127  clwwlknonex2lem2  30178  eucrctshift  30313  eucrct2eupth  30315  numclwwlk2lem1  30446  numclwwlk5lem  30457  frgrreggt1  30463  frgrreg  30464  friendship  30469  blocn2  30879  htthlem  30988  axhcompl-zf  31069  spanuni  31615  spansncol  31639  spansneleq  31641  elspansn5  31645  idcnop  32052  pjnormssi  32239  dmdmd  32371  bian1dOLD  32526  n0nsnel  32585  ifeqeqx  32612  opabssi  32686  ac6mapd  32696  ressupprn  32763  supxrnemnf  32841  rexdiv  32985  xrstos  33070  cnre2csqlem  34054  fsumcvg4  34094  lmxrge0  34096  qqhval2lem  34125  esumpr2  34211  esumcvg  34230  issgon  34267  measxun2  34354  measres  34366  measdivcst  34368  measdivcstALTV  34369  elorrvc  34608  signsply0  34695  bnj580  35055  nummin  35236  axprALT2  35253  0nn0m1nnn0  35295  umgracycusgr  35336  erdsze2lem2  35386  cvmsval  35448  fmlasuc  35568  fundmpss  35949  dfon2lem3  35965  dfrdg4  36133  cgrtriv  36184  btwntriv2  36194  ifscgr  36226  lineext  36258  btwnconn1lem12  36280  colinbtwnle  36300  elicc3  36499  ontgval  36613  onsucconni  36619  axtco1from2  36657  axtcond  36660  axnulregtco  36662  dfttc4lem2  36711  bj-bibibi  36851  bj-cbvalvv  36933  bj-cbval  36940  bj-cbvex  36941  bj-cbvexw  36971  bj-nnf-cbval  37077  bj-equsal  37133  bj-gabeqd  37244  bj-restn0  37402  bj-snmoore  37425  cgsex2gd  37451  bj-elsn0  37469  bj-finsumval0  37599  relowlssretop  37679  sucneqond  37681  finxpsuc  37714  pibt2  37733  wl-nfs1t  37862  finixpnum  37926  ltflcei  37929  matunitlindflem1  37937  poimirlem23  37964  poimirlem24  37965  poimirlem27  37968  poimirlem32  37973  itg2addnclem  37992  areacirclem2  38030  areacirclem5  38033  areacirc  38034  nninfnub  38072  prdstotbnd  38115  heiborlem4  38135  heibor  38142  elghomlem2OLD  38207  grpokerinj  38214  isidlc  38336  disjlem17  39223  prtlem17  39322  dral1-o  39350  axc16g-o  39380  lsator0sp  39447  atlrelat1  39767  cvratlem  39867  diaintclN  41504  dibintclN  41613  cdlemn11pre  41656  dihord2pre  41671  dihintcl  41790  dochkrshp4  41835  lcfrlem9  41996  lcfrlem21  42009  mapdh8e  42230  aks4d1p5  42519  aks6d1c1p1  42546  sticksstones4  42588  0prjspnrel  43060  elrfirn2  43128  rencldnfilem  43248  onsupnmax  43656  onov0suclim  43702  oege1  43734  cantnfresb  43752  dflim5  43757  omabs2  43760  refimssco  44034  rtrclex  44044  intimasn  44084  ss2iundf  44086  ov2ssiunov2  44127  comptiunov2i  44133  iunrelexpuztr  44146  dssmapf1od  44448  mnringmulrcld  44655  mnuprdlem1  44699  mnuprdlem2  44700  snelpwrVD  45257  en3lplem1VD  45269  en3lpVD  45271  orbi1rVD  45274  sbc3orgVD  45277  3impexpVD  45282  equncomVD  45294  trsbcVD  45303  trintALTVD  45306  trintALT  45307  csbingVD  45310  csbsngVD  45319  csbxpgVD  45320  csbrngVD  45322  csbfv12gALTVD  45325  relopabVD  45327  e2ebindVD  45338  xlimpnfxnegmnf  46242  xlimbr  46255  stoweidlem35  46463  stoweidlem48  46476  ormkglobd  47305  cjnpoly  47337  tannpoly  47338  n0nsn2el  47473  rexrsb  47548  2reu8i  47561  funbrafv  47606  rlimdmafv  47625  tz6.12c-afv2  47690  rlimdmafv2  47706  fzopredsuc  47772  2ffzoeq  47776  m1modnep2mod  47806  2timesltsq  47826  eqfvelsetpreimafv  47853  iccpartlt  47884  proththd  48077  even3prm2  48195  fppr2odd  48207  sbgoldbm  48260  nnsum3primesle9  48270  wtgoldbnnsum4prm  48278  bgoldbnnsum3prm  48280  grtrif1o  48418  mgm2mgm  48703  2zrngnmlid  48731  2zrngnmrid  48732  ellcoellss  48911  nneop  49002  fldivexpfllog2  49041  digexp  49083  reorelicc  49186  2itscp  49257  oppc1stflem  49762  prsthinc  49939  elpglem2  50187