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  1054  alexbii  1839  speivw  1982  spfw  2045  cbvalw  2047  alcomiw  2055  alcomiwOLD  2056  cbvalv1  2343  cbval  2398  axc16i  2436  sb3  2478  sb2  2480  axc16gALT  2494  eqrdav  2737  rspcimdv  3516  rspcedv  3519  moi2  3615  moi  3617  sspsstr  3996  2nreu  4331  rabsnifsb  4613  ralxfr2d  5277  axprlem4  5293  sbcop1  5345  isso2i  5477  wefrc  5519  elinxp  5863  sotri3  5964  oneqmini  6223  ordsssuc2  6260  ordtri2or  6267  iotan0  6329  2elresin  6457  f1ocnv  6630  tz6.12c  6699  fveqres  6716  fvun1  6759  dffo4  6879  funopsn  6920  fconst5  6978  fnprb  6981  fntpb  6982  isores3  7101  f1owe  7119  weniso  7120  ndmovordi  7355  abnexg  7497  orduniorsuc  7564  ordzsl  7579  tfinds  7593  dmfexALT  7641  f1oweALT  7698  opreuopreu  7759  fnse  7853  tposfo2  7944  wfrlem5  7988  wfrlem12  7995  issmo2  8015  iordsmo  8023  smoel2  8029  tz7.48lem  8106  oawordeulem  8211  om00  8232  omlimcl  8235  odi  8236  nnawordi  8278  unfi  8771  fiint  8869  fipreima  8903  dffi2  8960  suplub2  8998  wemapsolem  9087  unwdomg  9121  inf3lem3  9166  trcl  9243  fidomtri  9495  prdom2  9506  cardaleph  9589  ackbij1lem16  9735  coflim  9761  coftr  9773  infpssrlem4  9806  isfin7-2  9896  axdc3lem2  9951  axdc3lem4  9953  brdom6disj  10032  entric  10057  fpwwe2lem11  10141  inatsk  10278  grur1a  10319  indpi  10407  reclem3pr  10549  supsrlem  10611  lelttr  10809  dedekindle  10882  negn0  11147  fimaxre  11662  fiminre  11665  nnmulcl  11740  arch  11973  nnnegz  12065  zle0orge1  12079  zeo  12149  uzm1  12358  rpneg  12504  xrlttri  12615  xrlelttr  12632  iccid  12866  icoshft  12947  fzen  13015  elfz1b  13067  elfz2nn0  13089  fleqceilz  13313  zmodidfzoimp  13360  modsumfzodifsn  13403  hasheqf1oi  13804  hashnfinnn0  13814  hashle2prv  13930  swrd0  14109  pfxccatin12lem2  14182  swrdccat  14186  swrdccat3blem  14190  repswswrd  14235  trclublem  14444  max0add  14760  abslt  14764  absle  14765  rexuzre  14802  caurcvg  15126  caucvg  15128  dvdsval2  15702  negdvdsb  15718  muldvds2  15727  dvdsabseq  15758  smuval2  15925  smupvallem  15926  rplpwr  16003  alginv  16016  algfx  16021  coprmgcdb  16090  divgcdcoprm0  16106  oddprmgt2  16140  rpexp1i  16164  qnumdencl  16179  phiprmpw  16213  prmdiveq  16223  prm23lt5  16251  pcmpt  16328  infpnlem1  16346  prmgaplem3  16489  prmgaplem8  16494  imasaddfnlem  16904  plelttr  17698  lubval  17710  lublecllem  17714  glbval  17723  mndind  18108  mndodconglem  18787  sdrgacs  19699  elfrlmbasn0  20579  mavmulsolcl  21302  slesolex  21433  fvmptnn04if  21600  chfacfisf  21605  chfacfisfcpmat  21606  cnpnei  22015  unconn  22180  comppfsc  22283  kqsat  22482  isr0  22488  qtophmeo  22568  trufil  22661  alexsubALT  22802  cnextcn  22818  ucnima  23033  iducn  23035  bl2in  23153  addcnlem  23616  rescncf  23649  ovoliunlem2  24255  voliun  24306  mbflimsup  24418  itgcn  24597  dvdsq1p  24913  aalioulem2  25081  recosf1o  25279  logrec  25501  xrlimcnp  25706  basellem4  25821  bposlem1  26020  bposlem5  26024  lgsqrmod  26088  lgsdchrval  26090  2lgslem1a1  26125  pntlem3  26345  brbtwn2  26851  axbtwnid  26885  elntg2  26931  umgredgprv  27052  umgrpredgv  27085  usgredgprvALT  27137  fusgrfisstep  27271  fusgrfis  27272  nbupgr  27286  nbumgrvtx  27288  finsumvtxdg2size  27492  wlkp1lem8  27622  upgr2pthnlp  27673  wwlksnextinj  27837  usgr2wspthons3  27902  clwwlkccatlem  27926  clwlkclwwlklem2a1  27929  clwwisshclwws  27952  wwlksext2clwwlk  27994  clwwlknonex2lem2  28045  eucrctshift  28180  eucrct2eupth  28182  numclwwlk2lem1  28313  numclwwlk5lem  28324  frgrreggt1  28330  frgrreg  28331  friendship  28336  blocn2  28743  htthlem  28852  axhcompl-zf  28933  spanuni  29479  spansncol  29503  spansneleq  29505  elspansn5  29509  idcnop  29916  pjnormssi  30103  dmdmd  30235  bian1d  30382  ifeqeqx  30459  opabssi  30527  ressupprn  30599  supxrnemnf  30666  rexdiv  30775  xrstos  30865  xrge0omnd  30914  cnre2csqlem  31432  fsumcvg4  31472  lmxrge0  31474  qqhval2lem  31501  esumpr2  31605  esumcvg  31624  issgon  31661  measxun2  31748  measres  31760  measdivcst  31762  measdivcstALTV  31763  elorrvc  32000  signsply0  32100  bnj580  32464  nummin  32634  0nn0m1nnn0  32642  umgracycusgr  32687  erdsze2lem2  32737  cvmsval  32799  fmlasuc  32919  fundmpss  33312  dfon2lem3  33333  frmin  33390  sexp3  33410  poseq  33413  soseq  33414  fprlem1  33455  frrlem15  33460  nosupbnd1  33558  noinfbnd1  33573  oldbday  33719  lrcut  33721  dfrdg4  33891  cgrtriv  33942  btwntriv2  33952  ifscgr  33984  lineext  34016  btwnconn1lem12  34038  colinbtwnle  34058  elicc3  34144  ontgval  34258  onsucconni  34264  bj-bibibi  34406  bj-cbval  34468  bj-cbvex  34469  bj-cbvexw  34495  bj-equsal  34640  bj-restn0  34882  bj-snmoore  34905  bj-elsn0  34947  bj-finsumval0  35077  relowlssretop  35157  sucneqond  35159  finxpsuc  35192  pibt2  35211  wl-nfs1t  35319  finixpnum  35385  ltflcei  35388  matunitlindflem1  35396  poimirlem23  35423  poimirlem24  35424  poimirlem27  35427  poimirlem32  35432  itg2addnclem  35451  areacirclem2  35489  areacirclem5  35492  areacirc  35493  nninfnub  35532  prdstotbnd  35575  heiborlem4  35595  heibor  35602  elghomlem2OLD  35667  grpokerinj  35674  isidlc  35796  prtlem17  36513  dral1-o  36541  axc16g-o  36571  lsator0sp  36638  atlrelat1  36958  cvratlem  37058  diaintclN  38695  dibintclN  38804  cdlemn11pre  38847  dihord2pre  38862  dihintcl  38981  dochkrshp4  39026  lcfrlem9  39187  lcfrlem21  39200  mapdh8e  39421  sticksstones4  39711  metakunt29  39744  0prjspnrel  40041  elrfirn2  40090  rencldnfilem  40214  refimssco  40760  rtrclex  40770  intimasn  40811  ss2iundf  40813  ov2ssiunov2  40854  comptiunov2i  40860  iunrelexpuztr  40873  dssmapf1od  41175  mnringmulrcld  41388  mnuprdlem1  41432  mnuprdlem2  41433  snelpwrVD  41989  en3lplem1VD  42001  en3lpVD  42003  orbi1rVD  42006  sbc3orgVD  42009  3impexpVD  42014  equncomVD  42026  trsbcVD  42035  trintALTVD  42038  trintALT  42039  csbingVD  42042  csbsngVD  42051  csbxpgVD  42052  csbrngVD  42054  csbfv12gALTVD  42057  relopabVD  42059  e2ebindVD  42070  xlimpnfxnegmnf  42897  xlimbr  42910  stoweidlem35  43118  stoweidlem48  43131  rexrsb  44124  2reu8i  44138  funbrafv  44183  rlimdmafv  44202  tz6.12c-afv2  44267  rlimdmafv2  44283  fzopredsuc  44349  fzoopth  44353  2ffzoeq  44354  eqfvelsetpreimafv  44379  iccpartlt  44410  proththd  44600  even3prm2  44705  fppr2odd  44717  sbgoldbm  44770  nnsum3primesle9  44780  wtgoldbnnsum4prm  44788  bgoldbnnsum3prm  44790  mgm2mgm  44955  2zrngnmlid  45041  2zrngnmrid  45042  ellcoellss  45310  nneop  45406  fldivexpfllog2  45445  digexp  45487  reorelicc  45590  2itscp  45661  prsthinc  45799  elpglem2  45870