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  316  mtbid  323  mtbii  325  imbi1d  341  biimpar  477  prlem1  1051  alexbii  1836  speivw  1978  spfw  2037  cbvalw  2039  alcomiw  2047  alcomiwOLD  2048  cbvalv1  2340  cbval  2398  axc16i  2436  sb3  2478  sb2  2480  axc16gALT  2494  eqrdav  2737  ralbida  3156  rspcimdv  3541  rspcedv  3544  moi2  3646  moi  3648  sspsstr  4036  2nreu  4372  rabsnifsb  4655  ralxfr2d  5328  axprlem4  5344  sbcop1  5396  isso2i  5529  wefrc  5574  elinxp  5918  sotri3  6024  oneqmini  6302  ordsssuc2  6339  ordtri2or  6346  iotan0  6408  2elresin  6537  f1ocnv  6712  tz6.12c  6781  fveqres  6798  fvun1  6841  dffo4  6961  funopsn  7002  fconst5  7063  fnprb  7066  fntpb  7067  isores3  7186  f1owe  7204  weniso  7205  ndmovordi  7441  abnexg  7584  orduniorsuc  7652  ordzsl  7667  tfinds  7681  dmfexALT  7731  f1oweALT  7788  opreuopreu  7849  fnse  7945  tposfo2  8036  fprlem1  8087  wfrlem5OLD  8115  wfrlem12OLD  8122  issmo2  8151  iordsmo  8159  smoel2  8165  tz7.48lem  8242  oawordeulem  8347  om00  8368  omlimcl  8371  odi  8372  nnawordi  8414  unfi  8917  fiint  9021  fipreima  9055  dffi2  9112  suplub2  9150  wemapsolem  9239  unwdomg  9273  inf3lem3  9318  trcl  9417  frmin  9438  frrlem15  9446  fidomtri  9682  prdom2  9693  cardaleph  9776  ackbij1lem16  9922  coflim  9948  coftr  9960  infpssrlem4  9993  isfin7-2  10083  axdc3lem2  10138  axdc3lem4  10140  brdom6disj  10219  entric  10244  fpwwe2lem11  10328  inatsk  10465  grur1a  10506  indpi  10594  reclem3pr  10736  supsrlem  10798  lelttr  10996  dedekindle  11069  negn0  11334  fimaxre  11849  fiminre  11852  nnmulcl  11927  arch  12160  nnnegz  12252  zle0orge1  12266  zeo  12336  uzm1  12545  rpneg  12691  xrlttri  12802  xrlelttr  12819  iccid  13053  icoshft  13134  fzen  13202  elfz1b  13254  elfz2nn0  13276  fleqceilz  13502  zmodidfzoimp  13549  modsumfzodifsn  13592  hasheqf1oi  13994  hashnfinnn0  14004  hashle2prv  14120  swrd0  14299  pfxccatin12lem2  14372  swrdccat  14376  swrdccat3blem  14380  repswswrd  14425  trclublem  14634  max0add  14950  abslt  14954  absle  14955  rexuzre  14992  caurcvg  15316  caucvg  15318  dvdsval2  15894  negdvdsb  15910  muldvds2  15919  dvdsabseq  15950  smuval2  16117  smupvallem  16118  rplpwr  16195  alginv  16208  algfx  16213  coprmgcdb  16282  divgcdcoprm0  16298  oddprmgt2  16332  rpexp1i  16356  qnumdencl  16371  phiprmpw  16405  prmdiveq  16415  prm23lt5  16443  pcmpt  16521  infpnlem1  16539  prmgaplem3  16682  prmgaplem8  16687  imasaddfnlem  17156  plelttr  17977  lubval  17989  lublecllem  17993  glbval  18002  mndind  18381  mndodconglem  19064  sdrgacs  19984  elfrlmbasn0  20880  mavmulsolcl  21608  slesolex  21739  fvmptnn04if  21906  chfacfisf  21911  chfacfisfcpmat  21912  cnpnei  22323  unconn  22488  comppfsc  22591  kqsat  22790  isr0  22796  qtophmeo  22876  trufil  22969  alexsubALT  23110  cnextcn  23126  ucnima  23341  iducn  23343  bl2in  23461  addcnlem  23933  rescncf  23966  ovoliunlem2  24572  voliun  24623  mbflimsup  24735  itgcn  24914  dvdsq1p  25230  aalioulem2  25398  recosf1o  25596  logrec  25818  xrlimcnp  26023  basellem4  26138  bposlem1  26337  bposlem5  26341  lgsqrmod  26405  lgsdchrval  26407  2lgslem1a1  26442  pntlem3  26662  brbtwn2  27176  axbtwnid  27210  elntg2  27256  umgredgprv  27380  umgrpredgv  27413  usgredgprvALT  27465  fusgrfisstep  27599  fusgrfis  27600  nbupgr  27614  nbumgrvtx  27616  finsumvtxdg2size  27820  wlkp1lem8  27950  upgr2pthnlp  28001  wwlksnextinj  28165  usgr2wspthons3  28230  clwwlkccatlem  28254  clwlkclwwlklem2a1  28257  clwwisshclwws  28280  wwlksext2clwwlk  28322  clwwlknonex2lem2  28373  eucrctshift  28508  eucrct2eupth  28510  numclwwlk2lem1  28641  numclwwlk5lem  28652  frgrreggt1  28658  frgrreg  28659  friendship  28664  blocn2  29071  htthlem  29180  axhcompl-zf  29261  spanuni  29807  spansncol  29831  spansneleq  29833  elspansn5  29837  idcnop  30244  pjnormssi  30431  dmdmd  30563  bian1d  30710  ifeqeqx  30786  opabssi  30854  ressupprn  30926  supxrnemnf  30993  rexdiv  31102  xrstos  31190  xrge0omnd  31239  cnre2csqlem  31762  fsumcvg4  31802  lmxrge0  31804  qqhval2lem  31831  esumpr2  31935  esumcvg  31954  issgon  31991  measxun2  32078  measres  32090  measdivcst  32092  measdivcstALTV  32093  elorrvc  32330  signsply0  32430  bnj580  32793  nummin  32963  0nn0m1nnn0  32971  umgracycusgr  33016  erdsze2lem2  33066  cvmsval  33128  fmlasuc  33248  fundmpss  33646  dfon2lem3  33667  sexp3  33726  poseq  33729  soseq  33730  nosupbnd1  33844  noinfbnd1  33859  oldbday  34008  lrcut  34010  dfrdg4  34180  cgrtriv  34231  btwntriv2  34241  ifscgr  34273  lineext  34305  btwnconn1lem12  34327  colinbtwnle  34347  elicc3  34433  ontgval  34547  onsucconni  34553  bj-bibibi  34695  bj-cbval  34757  bj-cbvex  34758  bj-cbvexw  34784  bj-equsal  34936  bj-gabeqd  35052  bj-restn0  35188  bj-snmoore  35211  bj-elsn0  35253  bj-finsumval0  35383  relowlssretop  35461  sucneqond  35463  finxpsuc  35496  pibt2  35515  wl-nfs1t  35623  finixpnum  35689  ltflcei  35692  matunitlindflem1  35700  poimirlem23  35727  poimirlem24  35728  poimirlem27  35731  poimirlem32  35736  itg2addnclem  35755  areacirclem2  35793  areacirclem5  35796  areacirc  35797  nninfnub  35836  prdstotbnd  35879  heiborlem4  35899  heibor  35906  elghomlem2OLD  35971  grpokerinj  35978  isidlc  36100  prtlem17  36817  dral1-o  36845  axc16g-o  36875  lsator0sp  36942  atlrelat1  37262  cvratlem  37362  diaintclN  38999  dibintclN  39108  cdlemn11pre  39151  dihord2pre  39166  dihintcl  39285  dochkrshp4  39330  lcfrlem9  39491  lcfrlem21  39504  mapdh8e  39725  aks4d1p5  40016  sticksstones4  40033  metakunt29  40081  0prjspnrel  40385  elrfirn2  40434  rencldnfilem  40558  refimssco  41104  rtrclex  41114  intimasn  41154  ss2iundf  41156  ov2ssiunov2  41197  comptiunov2i  41203  iunrelexpuztr  41216  dssmapf1od  41518  mnringmulrcld  41735  mnuprdlem1  41779  mnuprdlem2  41780  snelpwrVD  42340  en3lplem1VD  42352  en3lpVD  42354  orbi1rVD  42357  sbc3orgVD  42360  3impexpVD  42365  equncomVD  42377  trsbcVD  42386  trintALTVD  42389  trintALT  42390  csbingVD  42393  csbsngVD  42402  csbxpgVD  42403  csbrngVD  42405  csbfv12gALTVD  42408  relopabVD  42410  e2ebindVD  42421  xlimpnfxnegmnf  43245  xlimbr  43258  stoweidlem35  43466  stoweidlem48  43479  rexrsb  44479  2reu8i  44492  funbrafv  44537  rlimdmafv  44556  tz6.12c-afv2  44621  rlimdmafv2  44637  fzopredsuc  44703  fzoopth  44707  2ffzoeq  44708  eqfvelsetpreimafv  44733  iccpartlt  44764  proththd  44954  even3prm2  45059  fppr2odd  45071  sbgoldbm  45124  nnsum3primesle9  45134  wtgoldbnnsum4prm  45142  bgoldbnnsum3prm  45144  mgm2mgm  45309  2zrngnmlid  45395  2zrngnmrid  45396  ellcoellss  45664  nneop  45760  fldivexpfllog2  45799  digexp  45841  reorelicc  45944  2itscp  46015  prsthinc  46223  elpglem2  46303