Theorem biimprd 248

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  biimtrrdi  254  mpbird  257  sylibrd  259  sylbird  260  con4bid  317  mtbid  324  mtbii  326  imbi1d  341  biimpar  477  prlem1  1054  alexbii  1833  speivw  1973  spfw  2032  cbvalw  2034  alcomimw  2042  cbvalv1  2342  cbval  2402  axc16i  2440  sb3  2481  sb2  2483  axc16gALT  2494  eqrdav  2734  ralbida  3253  rspcimdv  3591  rspcedv  3594  moi2  3699  moi  3701  sspsstr  4083  2nreu  4419  rabsnifsb  4698  ralxfr2d  5380  axprlem4OLD  5399  sbcop1  5463  isso2i  5598  wefrc  5648  elinxp  6006  sotri3  6119  oneqmini  6405  ordsssuc2  6444  ordtri2or  6451  iotan0  6520  2elresin  6658  f1ocnv  6829  tz6.12cOLD  6902  fveqres  6922  fvun1  6969  dffo4  7092  funopsn  7137  fconst5  7197  fnprb  7199  fntpb  7200  isores3  7327  f1owe  7345  weniso  7346  ndmovordi  7596  abnexg  7748  ordsuc  7805  orduniorsuc  7822  ordzsl  7838  tfinds  7853  dmfexALT  7902  f1oweALT  7969  opreuopreu  8031  fnse  8130  poxp3  8147  poseq  8155  soseq  8156  tposfo2  8246  fprlem1  8297  wfrlem5OLD  8325  wfrlem12OLD  8332  issmo2  8361  iordsmo  8369  smoel2  8375  tz7.48lem  8453  oawordeulem  8564  om00  8585  omlimcl  8588  odi  8589  nnawordi  8631  unfi  9183  php2  9220  fiint  9336  fiintOLD  9337  fipreima  9368  dffi2  9433  suplub2  9471  wemapsolem  9562  unwdomg  9596  inf3lem3  9642  trcl  9740  frrlem15  9769  fidomtri  10005  prdom2  10018  cardaleph  10101  ackbij1lem16  10246  coflim  10273  coftr  10285  infpssrlem4  10318  isfin7-2  10408  axdc3lem2  10463  axdc3lem4  10465  brdom6disj  10544  entric  10569  fpwwe2lem11  10653  inatsk  10790  grur1a  10831  indpi  10919  reclem3pr  11061  supsrlem  11123  lelttr  11323  dedekindle  11397  negn0  11664  fimaxre  12184  fiminre  12187  nnmulcl  12262  arch  12496  nnnegz  12589  zle0orge1  12603  zeo  12677  uzm1  12888  rpneg  13039  xrlttri  13153  xrlelttr  13170  iccid  13405  icoshft  13488  fzen  13556  elfz1b  13608  fzdif1  13620  elfz2nn0  13633  fzoopth  13776  fleqceilz  13869  zmodidfzoimp  13916  modsumfzodifsn  13960  hasheqf1oi  14367  hashnfinnn0  14377  hashle2prv  14494  swrd0  14674  pfxccatin12lem2  14747  swrdccat  14751  swrdccat3blem  14755  repswswrd  14800  trclublem  15012  max0add  15327  abslt  15331  absle  15332  rexuzre  15369  caurcvg  15691  caucvg  15693  dvdsval2  16273  negdvdsb  16290  muldvds2  16299  dvdsabseq  16330  smuval2  16499  smupvallem  16500  rplpwr  16575  alginv  16592  algfx  16597  coprmgcdb  16666  divgcdcoprm0  16682  oddprmgt2  16716  rpexp1i  16740  qnumdencl  16756  phiprmpw  16793  prmdiveq  16803  prm23lt5  16832  pcmpt  16910  infpnlem1  16928  prmgaplem3  17071  prmgaplem8  17076  imasaddfnlem  17540  plelttr  18352  lubval  18364  lublecllem  18368  glbval  18377  mndind  18804  mndodconglem  19520  sdrgacs  20759  elfrlmbasn0  21721  mavmulsolcl  22487  slesolex  22618  fvmptnn04if  22785  chfacfisf  22790  chfacfisfcpmat  22791  cnpnei  23200  unconn  23365  comppfsc  23468  kqsat  23667  isr0  23673  qtophmeo  23753  trufil  23846  alexsubALT  23987  cnextcn  24003  ucnima  24217  iducn  24219  bl2in  24337  addcnlem  24802  rescncf  24839  ovoliunlem2  25454  voliun  25505  mbflimsup  25617  itgcn  25796  dvdsq1p  26118  aalioulem2  26291  recosf1o  26494  logrec  26723  xrlimcnp  26928  basellem4  27044  bposlem1  27245  bposlem5  27249  lgsqrmod  27313  lgsdchrval  27315  2lgslem1a1  27350  pntlem3  27570  nosupbnd1  27676  noinfbnd1  27691  oldbday  27856  lrcut  27858  absslt  28190  brbtwn2  28830  axbtwnid  28864  elntg2  28910  umgredgprv  29032  umgrpredgv  29065  usgredgprvALT  29120  fusgrfisstep  29254  fusgrfis  29255  nbupgr  29269  nbumgrvtx  29271  finsumvtxdg2size  29476  wlkp1lem8  29606  upgr2pthnlp  29660  wwlksnextinj  29827  usgr2wspthons3  29892  clwwlkccatlem  29916  clwlkclwwlklem2a1  29919  clwwisshclwws  29942  wwlksext2clwwlk  29984  clwwlknonex2lem2  30035  eucrctshift  30170  eucrct2eupth  30172  numclwwlk2lem1  30303  numclwwlk5lem  30314  frgrreggt1  30320  frgrreg  30321  friendship  30326  blocn2  30735  htthlem  30844  axhcompl-zf  30925  spanuni  31471  spansncol  31495  spansneleq  31497  elspansn5  31501  idcnop  31908  pjnormssi  32095  dmdmd  32227  bian1dOLD  32384  n0nsnel  32442  ifeqeqx  32469  opabssi  32539  ac6mapd  32549  ressupprn  32613  supxrnemnf  32691  rexdiv  32846  xrstos  32948  xrge0omnd  33025  cnre2csqlem  33887  fsumcvg4  33927  lmxrge0  33929  qqhval2lem  33958  esumpr2  34044  esumcvg  34063  issgon  34100  measxun2  34187  measres  34199  measdivcst  34201  measdivcstALTV  34202  elorrvc  34442  signsply0  34529  bnj580  34890  nummin  35068  0nn0m1nnn0  35081  umgracycusgr  35122  erdsze2lem2  35172  cvmsval  35234  fmlasuc  35354  fundmpss  35730  dfon2lem3  35749  dfrdg4  35915  cgrtriv  35966  btwntriv2  35976  ifscgr  36008  lineext  36040  btwnconn1lem12  36062  colinbtwnle  36082  elicc3  36281  ontgval  36395  onsucconni  36401  bj-bibibi  36550  bj-cbval  36613  bj-cbvex  36614  bj-cbvexw  36640  bj-equsal  36790  bj-gabeqd  36901  bj-restn0  37054  bj-snmoore  37077  bj-elsn0  37119  bj-finsumval0  37249  relowlssretop  37327  sucneqond  37329  finxpsuc  37362  pibt2  37381  wl-nfs1t  37501  finixpnum  37575  ltflcei  37578  matunitlindflem1  37586  poimirlem23  37613  poimirlem24  37614  poimirlem27  37617  poimirlem32  37622  itg2addnclem  37641  areacirclem2  37679  areacirclem5  37682  areacirc  37683  nninfnub  37721  prdstotbnd  37764  heiborlem4  37784  heibor  37791  elghomlem2OLD  37856  grpokerinj  37863  isidlc  37985  disjlem17  38763  prtlem17  38840  dral1-o  38868  axc16g-o  38898  lsator0sp  38965  atlrelat1  39285  cvratlem  39386  diaintclN  41023  dibintclN  41132  cdlemn11pre  41175  dihord2pre  41190  dihintcl  41309  dochkrshp4  41354  lcfrlem9  41515  lcfrlem21  41528  mapdh8e  41749  aks4d1p5  42039  aks6d1c1p1  42066  sticksstones4  42108  metakunt29  42192  0prjspnrel  42597  elrfirn2  42666  rencldnfilem  42790  onsupnmax  43199  onov0suclim  43245  oege1  43277  cantnfresb  43295  dflim5  43300  omabs2  43303  refimssco  43578  rtrclex  43588  intimasn  43628  ss2iundf  43630  ov2ssiunov2  43671  comptiunov2i  43677  iunrelexpuztr  43690  dssmapf1od  43992  mnringmulrcld  44200  mnuprdlem1  44244  mnuprdlem2  44245  snelpwrVD  44803  en3lplem1VD  44815  en3lpVD  44817  orbi1rVD  44820  sbc3orgVD  44823  3impexpVD  44828  equncomVD  44840  trsbcVD  44849  trintALTVD  44852  trintALT  44853  csbingVD  44856  csbsngVD  44865  csbxpgVD  44866  csbrngVD  44868  csbfv12gALTVD  44871  relopabVD  44873  e2ebindVD  44884  xlimpnfxnegmnf  45791  xlimbr  45804  stoweidlem35  46012  stoweidlem48  46025  ormkglobd  46852  n0nsn2el  47002  rexrsb  47077  2reu8i  47090  funbrafv  47135  rlimdmafv  47154  tz6.12c-afv2  47219  rlimdmafv2  47235  fzopredsuc  47300  2ffzoeq  47304  m1modnep2mod  47329  eqfvelsetpreimafv  47355  iccpartlt  47386  proththd  47576  even3prm2  47681  fppr2odd  47693  sbgoldbm  47746  nnsum3primesle9  47756  wtgoldbnnsum4prm  47764  bgoldbnnsum3prm  47766  grtrif1o  47902  mgm2mgm  48150  2zrngnmlid  48178  2zrngnmrid  48179  ellcoellss  48359  nneop  48454  fldivexpfllog2  48493  digexp  48535  reorelicc  48638  2itscp  48709  prsthinc  49298  elpglem2  49524