Theorem biimprd 250

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  syl6bir  256  mpbird  259  sylibrd  261  sylbird  262  con4bid  319  mtbid  326  mtbii  328  imbi1d  344  biimpar  480  prlem1  1049  alexbii  1833  speivw  1977  spfw  2040  cbvalw  2042  alcomiw  2050  alcomiwOLD  2051  sbbidvOLD  2085  sbbidOLD  2248  cbvalv1  2361  cbval  2416  axc16i  2458  sb3  2502  sb2  2504  axc16gALT  2529  eqrdav  2820  pm13.18OLD  3098  rspcimdv  3613  rspcedv  3616  moi2  3707  moi  3709  sspsstr  4082  2nreu  4393  rabsnifsb  4658  eldifsnneqOLD  4724  ralxfr2d  5311  axprlem4  5327  sbcop1  5379  isso2i  5508  wefrc  5549  elinxp  5890  sotri3  5990  oneqmini  6242  ordsssuc2  6279  ordtri2or  6286  iotan0  6345  2elresin  6468  f1ocnv  6627  tz6.12c  6695  fveqres  6712  fvun1  6754  dffo4  6869  funopsn  6910  fconst5  6968  fnprb  6971  fntpb  6972  isores3  7088  f1owe  7106  weniso  7107  ndmovordi  7339  abnexg  7478  orduniorsuc  7545  ordzsl  7560  tfinds  7574  f1oweALT  7673  opreuopreu  7734  fnse  7827  tposfo2  7915  wfrlem5  7959  wfrlem12  7966  issmo2  7986  iordsmo  7994  smoel2  8000  tz7.48lem  8077  oawordeulem  8180  om00  8201  omlimcl  8204  odi  8205  nnawordi  8247  fiint  8795  fipreima  8830  dffi2  8887  suplub2  8925  wemapsolem  9014  unwdomg  9048  inf3lem3  9093  trcl  9170  fidomtri  9422  prdom2  9432  cardaleph  9515  ackbij1lem16  9657  coflim  9683  coftr  9695  infpssrlem4  9728  isfin7-2  9818  axdc3lem2  9873  axdc3lem4  9875  brdom6disj  9954  entric  9979  fpwwe2lem12  10063  inatsk  10200  grur1a  10241  indpi  10329  reclem3pr  10471  supsrlem  10533  lelttr  10731  dedekindle  10804  negn0  11069  fimaxre  11584  fimaxreOLD  11585  fiminre  11588  nnmulcl  11662  arch  11895  nnnegz  11985  zle0orge1  11999  zeo  12069  uzm1  12277  rpneg  12422  xrlttri  12533  xrlelttr  12550  iccid  12784  icoshft  12860  fzen  12925  elfz1b  12977  elfz2nn0  12999  fleqceilz  13223  zmodidfzoimp  13270  modsumfzodifsn  13313  hasheqf1oi  13713  hashnfinnn0  13723  hashle2prv  13837  swrd0  14020  pfxccatin12lem2  14093  swrdccat  14097  swrdccat3blem  14101  repswswrd  14146  trclublem  14355  max0add  14670  abslt  14674  absle  14675  rexuzre  14712  caurcvg  15033  caucvg  15035  dvdsval2  15610  negdvdsb  15626  muldvds2  15635  dvdsabseq  15663  smuval2  15831  smupvallem  15832  rplpwr  15907  alginv  15919  algfx  15924  coprmgcdb  15993  divgcdcoprm0  16009  oddprmgt2  16043  rpexp1i  16065  qnumdencl  16079  phiprmpw  16113  prmdiveq  16123  prm23lt5  16151  pcmpt  16228  infpnlem1  16246  prmgaplem3  16389  prmgaplem8  16394  imasaddfnlem  16801  plelttr  17582  lubval  17594  lublecllem  17598  glbval  17607  mndind  17992  mndodconglem  18669  sdrgacs  19580  elfrlmbasn0  20907  mavmulsolcl  21160  slesolex  21291  fvmptnn04if  21457  chfacfisf  21462  chfacfisfcpmat  21463  cnpnei  21872  unconn  22037  comppfsc  22140  kqsat  22339  isr0  22345  qtophmeo  22425  trufil  22518  alexsubALT  22659  cnextcn  22675  ucnima  22890  iducn  22892  bl2in  23010  addcnlem  23472  rescncf  23505  ovoliunlem2  24104  voliun  24155  mbflimsup  24267  itgcn  24443  dvdsq1p  24754  aalioulem2  24922  recosf1o  25119  logrec  25341  xrlimcnp  25546  basellem4  25661  bposlem1  25860  bposlem5  25864  lgsqrmod  25928  lgsdchrval  25930  2lgslem1a1  25965  pntlem3  26185  brbtwn2  26691  axbtwnid  26725  elntg2  26771  umgredgprv  26892  umgrpredgv  26925  usgredgprvALT  26977  fusgrfisstep  27111  fusgrfis  27112  nbupgr  27126  nbumgrvtx  27128  finsumvtxdg2size  27332  wlkp1lem8  27462  upgr2pthnlp  27513  wwlksnextinj  27677  usgr2wspthons3  27743  clwwlkccatlem  27767  clwlkclwwlklem2a1  27770  clwwisshclwws  27793  wwlksext2clwwlk  27836  clwwlknonex2lem2  27887  eucrctshift  28022  eucrct2eupth  28024  numclwwlk2lem1  28155  numclwwlk5lem  28166  frgrreggt1  28172  frgrreg  28173  friendship  28178  blocn2  28585  htthlem  28694  axhcompl-zf  28775  spanuni  29321  spansncol  29345  spansneleq  29347  elspansn5  29351  idcnop  29758  pjnormssi  29945  dmdmd  30077  bian1d  30224  ifeqeqx  30297  opabssi  30364  supxrnemnf  30493  rexdiv  30602  xrstos  30666  xrge0omnd  30712  cnre2csqlem  31153  fsumcvg4  31193  lmxrge0  31195  qqhval2lem  31222  esumpr2  31326  esumcvg  31345  issgon  31382  measxun2  31469  measres  31481  measdivcst  31483  measdivcstALTV  31484  elorrvc  31721  signsply0  31821  bnj580  32185  0nn0m1nnn0  32351  umgracycusgr  32401  erdsze2lem2  32451  cvmsval  32513  fmlasuc  32633  fundmpss  33009  dfon2lem3  33030  frmin  33084  poseq  33095  soseq  33096  fprlem1  33137  frrlem15  33142  nosupbnd1  33214  dfrdg4  33412  cgrtriv  33463  btwntriv2  33473  ifscgr  33505  lineext  33537  btwnconn1lem12  33559  colinbtwnle  33579  elicc3  33665  ontgval  33779  onsucconni  33785  bj-bibibi  33920  bj-cbval  33982  bj-cbvex  33983  bj-cbvexw  34009  bj-equsal  34149  bj-restn0  34384  bj-snmoore  34408  bj-elsn0  34450  bj-finsumval0  34570  relowlssretop  34647  sucneqond  34649  finxpsuc  34682  pibt2  34701  wl-nfs1t  34792  finixpnum  34892  ltflcei  34895  matunitlindflem1  34903  poimirlem23  34930  poimirlem24  34931  poimirlem27  34934  poimirlem32  34939  itg2addnclem  34958  areacirclem2  34998  areacirclem5  35001  areacirc  35002  nninfnub  35041  prdstotbnd  35087  heiborlem4  35107  heibor  35114  elghomlem2OLD  35179  grpokerinj  35186  isidlc  35308  prtlem17  36027  dral1-o  36055  axc16g-o  36085  lsator0sp  36152  atlrelat1  36472  cvratlem  36572  diaintclN  38209  dibintclN  38318  cdlemn11pre  38361  dihord2pre  38376  dihintcl  38495  dochkrshp4  38540  lcfrlem9  38701  lcfrlem21  38714  mapdh8e  38935  0prjspnrel  39318  elrfirn2  39342  rencldnfilem  39466  refimssco  40016  rtrclex  40026  intimasn  40051  ss2iundf  40053  ov2ssiunov2  40094  comptiunov2i  40100  iunrelexpuztr  40113  dssmapf1od  40416  mnuprdlem1  40657  mnuprdlem2  40658  snelpwrVD  41214  en3lplem1VD  41226  en3lpVD  41228  orbi1rVD  41231  sbc3orgVD  41234  3impexpVD  41239  equncomVD  41251  trsbcVD  41260  trintALTVD  41263  trintALT  41264  csbingVD  41267  csbsngVD  41276  csbxpgVD  41277  csbrngVD  41279  csbfv12gALTVD  41282  relopabVD  41284  e2ebindVD  41295  xlimpnfxnegmnf  42144  xlimbr  42157  stoweidlem35  42369  stoweidlem48  42382  rexrsb  43347  2reu8i  43361  funbrafv  43406  rlimdmafv  43425  tz6.12c-afv2  43490  rlimdmafv2  43506  fzopredsuc  43572  fzoopth  43576  2ffzoeq  43577  eqfvelsetpreimafv  43602  iccpartlt  43633  proththd  43828  even3prm2  43933  fppr2odd  43945  sbgoldbm  43998  nnsum3primesle9  44008  wtgoldbnnsum4prm  44016  bgoldbnnsum3prm  44018  mgm2mgm  44183  2zrngnmlid  44269  2zrngnmrid  44270  ellcoellss  44539  nneop  44635  fldivexpfllog2  44674  digexp  44716  reorelicc  44746  2itscp  44817  elpglem2  44863