Theorem biimprd 247

Description: Deduce a converse implication from a logical equivalence. Deduction associated with biimpr 219 and biimpri 227. (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	syl5ibr 245	1 ⊢ (𝜑 → (𝜒 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  syl6bir  253  mpbird  256  sylibrd  258  sylbird  259  con4bid  317  mtbid  324  mtbii  326  imbi1d  342  biimpar  478  prlem1  1052  alexbii  1836  speivw  1978  spfw  2037  cbvalw  2039  alcomiw  2047  alcomiwOLD  2048  cbvalv1  2339  cbval  2399  axc16i  2437  sb3  2479  sb2  2481  axc16gALT  2495  eqrdav  2738  ralbida  3160  rspcimdv  3552  rspcedv  3555  moi2  3652  moi  3654  sspsstr  4041  2nreu  4376  rabsnifsb  4659  ralxfr2d  5334  axprlem4  5350  sbcop1  5403  isso2i  5539  wefrc  5584  elinxp  5932  sotri3  6040  oneqmini  6321  ordsssuc2  6358  ordtri2or  6365  iotan0  6427  2elresin  6562  f1ocnv  6737  tz6.12c  6808  fveqres  6825  fvun1  6868  dffo4  6988  funopsn  7029  fconst5  7090  fnprb  7093  fntpb  7094  isores3  7215  f1owe  7233  weniso  7234  ndmovordi  7472  abnexg  7615  orduniorsuc  7686  ordzsl  7701  tfinds  7715  dmfexALT  7766  f1oweALT  7824  opreuopreu  7885  fnse  7983  tposfo2  8074  fprlem1  8125  wfrlem5OLD  8153  wfrlem12OLD  8160  issmo2  8189  iordsmo  8197  smoel2  8203  tz7.48lem  8281  oawordeulem  8394  om00  8415  omlimcl  8418  odi  8419  nnawordi  8461  unfi  8964  php2  9003  fiint  9100  fipreima  9134  dffi2  9191  suplub2  9229  wemapsolem  9318  unwdomg  9352  inf3lem3  9397  trcl  9495  frrlem15  9524  fidomtri  9760  prdom2  9771  cardaleph  9854  ackbij1lem16  10000  coflim  10026  coftr  10038  infpssrlem4  10071  isfin7-2  10161  axdc3lem2  10216  axdc3lem4  10218  brdom6disj  10297  entric  10322  fpwwe2lem11  10406  inatsk  10543  grur1a  10584  indpi  10672  reclem3pr  10814  supsrlem  10876  lelttr  11074  dedekindle  11148  negn0  11413  fimaxre  11928  fiminre  11931  nnmulcl  12006  arch  12239  nnnegz  12331  zle0orge1  12345  zeo  12415  uzm1  12625  rpneg  12771  xrlttri  12882  xrlelttr  12899  iccid  13133  icoshft  13214  fzen  13282  elfz1b  13334  elfz2nn0  13356  fleqceilz  13583  zmodidfzoimp  13630  modsumfzodifsn  13673  hasheqf1oi  14075  hashnfinnn0  14085  hashle2prv  14201  swrd0  14380  pfxccatin12lem2  14453  swrdccat  14457  swrdccat3blem  14461  repswswrd  14506  trclublem  14715  max0add  15031  abslt  15035  absle  15036  rexuzre  15073  caurcvg  15397  caucvg  15399  dvdsval2  15975  negdvdsb  15991  muldvds2  16000  dvdsabseq  16031  smuval2  16198  smupvallem  16199  rplpwr  16276  alginv  16289  algfx  16294  coprmgcdb  16363  divgcdcoprm0  16379  oddprmgt2  16413  rpexp1i  16437  qnumdencl  16452  phiprmpw  16486  prmdiveq  16496  prm23lt5  16524  pcmpt  16602  infpnlem1  16620  prmgaplem3  16763  prmgaplem8  16768  imasaddfnlem  17248  plelttr  18071  lubval  18083  lublecllem  18087  glbval  18096  mndind  18475  mndodconglem  19158  sdrgacs  20078  elfrlmbasn0  20979  mavmulsolcl  21709  slesolex  21840  fvmptnn04if  22007  chfacfisf  22012  chfacfisfcpmat  22013  cnpnei  22424  unconn  22589  comppfsc  22692  kqsat  22891  isr0  22897  qtophmeo  22977  trufil  23070  alexsubALT  23211  cnextcn  23227  ucnima  23442  iducn  23444  bl2in  23562  addcnlem  24036  rescncf  24069  ovoliunlem2  24676  voliun  24727  mbflimsup  24839  itgcn  25018  dvdsq1p  25334  aalioulem2  25502  recosf1o  25700  logrec  25922  xrlimcnp  26127  basellem4  26242  bposlem1  26441  bposlem5  26445  lgsqrmod  26509  lgsdchrval  26511  2lgslem1a1  26546  pntlem3  26766  brbtwn2  27282  axbtwnid  27316  elntg2  27362  umgredgprv  27486  umgrpredgv  27519  usgredgprvALT  27571  fusgrfisstep  27705  fusgrfis  27706  nbupgr  27720  nbumgrvtx  27722  finsumvtxdg2size  27926  wlkp1lem8  28057  upgr2pthnlp  28109  wwlksnextinj  28273  usgr2wspthons3  28338  clwwlkccatlem  28362  clwlkclwwlklem2a1  28365  clwwisshclwws  28388  wwlksext2clwwlk  28430  clwwlknonex2lem2  28481  eucrctshift  28616  eucrct2eupth  28618  numclwwlk2lem1  28749  numclwwlk5lem  28760  frgrreggt1  28766  frgrreg  28767  friendship  28772  blocn2  29179  htthlem  29288  axhcompl-zf  29369  spanuni  29915  spansncol  29939  spansneleq  29941  elspansn5  29945  idcnop  30352  pjnormssi  30539  dmdmd  30671  bian1d  30818  ifeqeqx  30894  opabssi  30962  ressupprn  31033  supxrnemnf  31100  rexdiv  31209  xrstos  31297  xrge0omnd  31346  cnre2csqlem  31869  fsumcvg4  31909  lmxrge0  31911  qqhval2lem  31940  esumpr2  32044  esumcvg  32063  issgon  32100  measxun2  32187  measres  32199  measdivcst  32201  measdivcstALTV  32202  elorrvc  32439  signsply0  32539  bnj580  32902  nummin  33072  0nn0m1nnn0  33080  umgracycusgr  33125  erdsze2lem2  33175  cvmsval  33237  fmlasuc  33357  fundmpss  33749  dfon2lem3  33770  sexp3  33808  poseq  33811  soseq  33812  nosupbnd1  33926  noinfbnd1  33941  oldbday  34090  lrcut  34092  dfrdg4  34262  cgrtriv  34313  btwntriv2  34323  ifscgr  34355  lineext  34387  btwnconn1lem12  34409  colinbtwnle  34429  elicc3  34515  ontgval  34629  onsucconni  34635  bj-bibibi  34777  bj-cbval  34839  bj-cbvex  34840  bj-cbvexw  34866  bj-equsal  35018  bj-gabeqd  35134  bj-restn0  35270  bj-snmoore  35293  bj-elsn0  35335  bj-finsumval0  35465  relowlssretop  35543  sucneqond  35545  finxpsuc  35578  pibt2  35597  wl-nfs1t  35705  finixpnum  35771  ltflcei  35774  matunitlindflem1  35782  poimirlem23  35809  poimirlem24  35810  poimirlem27  35813  poimirlem32  35818  itg2addnclem  35837  areacirclem2  35875  areacirclem5  35878  areacirc  35879  nninfnub  35918  prdstotbnd  35961  heiborlem4  35981  heibor  35988  elghomlem2OLD  36053  grpokerinj  36060  isidlc  36182  prtlem17  36897  dral1-o  36925  axc16g-o  36955  lsator0sp  37022  atlrelat1  37342  cvratlem  37442  diaintclN  39079  dibintclN  39188  cdlemn11pre  39231  dihord2pre  39246  dihintcl  39365  dochkrshp4  39410  lcfrlem9  39571  lcfrlem21  39584  mapdh8e  39805  aks4d1p5  40095  sticksstones4  40112  metakunt29  40160  0prjspnrel  40471  elrfirn2  40525  rencldnfilem  40649  refimssco  41222  rtrclex  41232  intimasn  41272  ss2iundf  41274  ov2ssiunov2  41315  comptiunov2i  41321  iunrelexpuztr  41334  dssmapf1od  41636  mnringmulrcld  41853  mnuprdlem1  41897  mnuprdlem2  41898  snelpwrVD  42458  en3lplem1VD  42470  en3lpVD  42472  orbi1rVD  42475  sbc3orgVD  42478  3impexpVD  42483  equncomVD  42495  trsbcVD  42504  trintALTVD  42507  trintALT  42508  csbingVD  42511  csbsngVD  42520  csbxpgVD  42521  csbrngVD  42523  csbfv12gALTVD  42526  relopabVD  42528  e2ebindVD  42539  xlimpnfxnegmnf  43362  xlimbr  43375  stoweidlem35  43583  stoweidlem48  43596  rexrsb  44603  2reu8i  44616  funbrafv  44661  rlimdmafv  44680  tz6.12c-afv2  44745  rlimdmafv2  44761  fzopredsuc  44826  fzoopth  44830  2ffzoeq  44831  eqfvelsetpreimafv  44856  iccpartlt  44887  proththd  45077  even3prm2  45182  fppr2odd  45194  sbgoldbm  45247  nnsum3primesle9  45257  wtgoldbnnsum4prm  45265  bgoldbnnsum3prm  45267  mgm2mgm  45432  2zrngnmlid  45518  2zrngnmrid  45519  ellcoellss  45787  nneop  45883  fldivexpfllog2  45922  digexp  45964  reorelicc  46067  2itscp  46138  prsthinc  46346  elpglem2  46428