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 22	. 2 ⊢ (𝜒 → 𝜒)
2		biimprd.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	syl5ibr 249	1 ⊢ (𝜑 → (𝜒 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  syl6bir  257  mpbird  260  sylibrd  262  sylbird  263  con4bid  320  mtbid  327  mtbii  329  imbi1d  345  biimpar  481  prlem1  1050  alexbii  1834  speivw  1977  spfw  2040  cbvalw  2042  alcomiw  2050  alcomiwOLD  2051  cbvalv1  2350  cbval  2405  axc16i  2447  sb3  2491  sb2  2493  axc16gALT  2508  eqrdav  2797  rspcimdv  3561  rspcedv  3564  moi2  3655  moi  3657  sspsstr  4033  2nreu  4349  rabsnifsb  4618  ralxfr2d  5276  axprlem4  5292  sbcop1  5344  isso2i  5472  wefrc  5513  elinxp  5856  sotri3  5957  oneqmini  6210  ordsssuc2  6247  ordtri2or  6254  iotan0  6314  2elresin  6440  f1ocnv  6602  tz6.12c  6670  fveqres  6687  fvun1  6729  dffo4  6846  funopsn  6887  fconst5  6945  fnprb  6948  fntpb  6949  isores3  7067  f1owe  7085  weniso  7086  ndmovordi  7319  abnexg  7458  orduniorsuc  7525  ordzsl  7540  tfinds  7554  f1oweALT  7655  opreuopreu  7716  fnse  7810  tposfo2  7898  wfrlem5  7942  wfrlem12  7949  issmo2  7969  iordsmo  7977  smoel2  7983  tz7.48lem  8060  oawordeulem  8163  om00  8184  omlimcl  8187  odi  8188  nnawordi  8230  fiint  8779  fipreima  8814  dffi2  8871  suplub2  8909  wemapsolem  8998  unwdomg  9032  inf3lem3  9077  trcl  9154  fidomtri  9406  prdom2  9417  cardaleph  9500  ackbij1lem16  9646  coflim  9672  coftr  9684  infpssrlem4  9717  isfin7-2  9807  axdc3lem2  9862  axdc3lem4  9864  brdom6disj  9943  entric  9968  fpwwe2lem12  10052  inatsk  10189  grur1a  10230  indpi  10318  reclem3pr  10460  supsrlem  10522  lelttr  10720  dedekindle  10793  negn0  11058  fimaxre  11573  fiminre  11576  nnmulcl  11649  arch  11882  nnnegz  11972  zle0orge1  11986  zeo  12056  uzm1  12264  rpneg  12409  xrlttri  12520  xrlelttr  12537  iccid  12771  icoshft  12851  fzen  12919  elfz1b  12971  elfz2nn0  12993  fleqceilz  13217  zmodidfzoimp  13264  modsumfzodifsn  13307  hasheqf1oi  13708  hashnfinnn0  13718  hashle2prv  13832  swrd0  14011  pfxccatin12lem2  14084  swrdccat  14088  swrdccat3blem  14092  repswswrd  14137  trclublem  14346  max0add  14662  abslt  14666  absle  14667  rexuzre  14704  caurcvg  15025  caucvg  15027  dvdsval2  15602  negdvdsb  15618  muldvds2  15627  dvdsabseq  15655  smuval2  15821  smupvallem  15822  rplpwr  15897  alginv  15909  algfx  15914  coprmgcdb  15983  divgcdcoprm0  15999  oddprmgt2  16033  rpexp1i  16055  qnumdencl  16069  phiprmpw  16103  prmdiveq  16113  prm23lt5  16141  pcmpt  16218  infpnlem1  16236  prmgaplem3  16379  prmgaplem8  16384  imasaddfnlem  16793  plelttr  17574  lubval  17586  lublecllem  17590  glbval  17599  mndind  17984  mndodconglem  18661  sdrgacs  19573  elfrlmbasn0  20452  mavmulsolcl  21156  slesolex  21287  fvmptnn04if  21454  chfacfisf  21459  chfacfisfcpmat  21460  cnpnei  21869  unconn  22034  comppfsc  22137  kqsat  22336  isr0  22342  qtophmeo  22422  trufil  22515  alexsubALT  22656  cnextcn  22672  ucnima  22887  iducn  22889  bl2in  23007  addcnlem  23469  rescncf  23502  ovoliunlem2  24107  voliun  24158  mbflimsup  24270  itgcn  24448  dvdsq1p  24761  aalioulem2  24929  recosf1o  25127  logrec  25349  xrlimcnp  25554  basellem4  25669  bposlem1  25868  bposlem5  25872  lgsqrmod  25936  lgsdchrval  25938  2lgslem1a1  25973  pntlem3  26193  brbtwn2  26699  axbtwnid  26733  elntg2  26779  umgredgprv  26900  umgrpredgv  26933  usgredgprvALT  26985  fusgrfisstep  27119  fusgrfis  27120  nbupgr  27134  nbumgrvtx  27136  finsumvtxdg2size  27340  wlkp1lem8  27470  upgr2pthnlp  27521  wwlksnextinj  27685  usgr2wspthons3  27750  clwwlkccatlem  27774  clwlkclwwlklem2a1  27777  clwwisshclwws  27800  wwlksext2clwwlk  27842  clwwlknonex2lem2  27893  eucrctshift  28028  eucrct2eupth  28030  numclwwlk2lem1  28161  numclwwlk5lem  28172  frgrreggt1  28178  frgrreg  28179  friendship  28184  blocn2  28591  htthlem  28700  axhcompl-zf  28781  spanuni  29327  spansncol  29351  spansneleq  29353  elspansn5  29357  idcnop  29764  pjnormssi  29951  dmdmd  30083  bian1d  30230  ifeqeqx  30309  opabssi  30377  ressupprn  30450  supxrnemnf  30519  rexdiv  30628  xrstos  30713  xrge0omnd  30762  cnre2csqlem  31263  fsumcvg4  31303  lmxrge0  31305  qqhval2lem  31332  esumpr2  31436  esumcvg  31455  issgon  31492  measxun2  31579  measres  31591  measdivcst  31593  measdivcstALTV  31594  elorrvc  31831  signsply0  31931  bnj580  32295  0nn0m1nnn0  32461  nummin  32474  umgracycusgr  32514  erdsze2lem2  32564  cvmsval  32626  fmlasuc  32746  fundmpss  33122  dfon2lem3  33143  frmin  33197  poseq  33208  soseq  33209  fprlem1  33250  frrlem15  33255  nosupbnd1  33327  dfrdg4  33525  cgrtriv  33576  btwntriv2  33586  ifscgr  33618  lineext  33650  btwnconn1lem12  33672  colinbtwnle  33692  elicc3  33778  ontgval  33892  onsucconni  33898  bj-bibibi  34033  bj-cbval  34095  bj-cbvex  34096  bj-cbvexw  34122  bj-equsal  34264  bj-restn0  34505  bj-snmoore  34528  bj-elsn0  34570  bj-finsumval0  34700  relowlssretop  34780  sucneqond  34782  finxpsuc  34815  pibt2  34834  wl-nfs1t  34942  finixpnum  35042  ltflcei  35045  matunitlindflem1  35053  poimirlem23  35080  poimirlem24  35081  poimirlem27  35084  poimirlem32  35089  itg2addnclem  35108  areacirclem2  35146  areacirclem5  35149  areacirc  35150  nninfnub  35189  prdstotbnd  35232  heiborlem4  35252  heibor  35259  elghomlem2OLD  35324  grpokerinj  35331  isidlc  35453  prtlem17  36172  dral1-o  36200  axc16g-o  36230  lsator0sp  36297  atlrelat1  36617  cvratlem  36717  diaintclN  38354  dibintclN  38463  cdlemn11pre  38506  dihord2pre  38521  dihintcl  38640  dochkrshp4  38685  lcfrlem9  38846  lcfrlem21  38859  mapdh8e  39080  metakunt29  39378  0prjspnrel  39613  elrfirn2  39637  rencldnfilem  39761  refimssco  40307  rtrclex  40317  intimasn  40358  ss2iundf  40360  ov2ssiunov2  40401  comptiunov2i  40407  iunrelexpuztr  40420  dssmapf1od  40722  mnringmulrcld  40936  mnuprdlem1  40980  mnuprdlem2  40981  snelpwrVD  41537  en3lplem1VD  41549  en3lpVD  41551  orbi1rVD  41554  sbc3orgVD  41557  3impexpVD  41562  equncomVD  41574  trsbcVD  41583  trintALTVD  41586  trintALT  41587  csbingVD  41590  csbsngVD  41599  csbxpgVD  41600  csbrngVD  41602  csbfv12gALTVD  41605  relopabVD  41607  e2ebindVD  41618  xlimpnfxnegmnf  42456  xlimbr  42469  stoweidlem35  42677  stoweidlem48  42690  rexrsb  43655  2reu8i  43669  funbrafv  43714  rlimdmafv  43733  tz6.12c-afv2  43798  rlimdmafv2  43814  fzopredsuc  43880  fzoopth  43884  2ffzoeq  43885  eqfvelsetpreimafv  43910  iccpartlt  43941  proththd  44132  even3prm2  44237  fppr2odd  44249  sbgoldbm  44302  nnsum3primesle9  44312  wtgoldbnnsum4prm  44320  bgoldbnnsum3prm  44322  mgm2mgm  44487  2zrngnmlid  44573  2zrngnmrid  44574  ellcoellss  44844  nneop  44940  fldivexpfllog2  44979  digexp  45021  reorelicc  45124  2itscp  45195  elpglem2  45241