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  2033  cbvalw  2035  alcomimw  2043  cbvalv1  2339  cbval  2396  axc16i  2434  sb3  2475  sb2  2477  axc16gALT  2488  eqrdav  2728  ralbida  3246  rspcimdv  3575  rspcedv  3578  moi2  3684  moi  3686  sspsstr  4067  2nreu  4403  rabsnifsb  4682  ralxfr2d  5360  axprlem4OLD  5379  sbcop1  5443  isso2i  5576  wefrc  5625  elinxp  5979  sotri3  6091  oneqmini  6373  ordsssuc2  6413  ordtri2or  6420  iotan0  6489  2elresin  6621  f1ocnv  6794  tz6.12cOLD  6867  fveqres  6887  fvun1  6934  dffo4  7057  funopsn  7102  fconst5  7162  fnprb  7164  fntpb  7165  isores3  7292  f1owe  7310  weniso  7311  ndmovordi  7560  abnexg  7712  ordsuc  7768  orduniorsuc  7785  ordzsl  7801  tfinds  7816  dmfexALT  7864  f1oweALT  7930  opreuopreu  7992  fnse  8089  poxp3  8106  poseq  8114  soseq  8115  tposfo2  8205  fprlem1  8256  issmo2  8295  iordsmo  8303  smoel2  8309  tz7.48lem  8386  oawordeulem  8495  om00  8516  omlimcl  8519  odi  8520  nnawordi  8562  unfi  9112  php2  9149  fiint  9253  fiintOLD  9254  fipreima  9285  dffi2  9350  suplub2  9388  wemapsolem  9479  unwdomg  9513  inf3lem3  9559  trcl  9657  frrlem15  9686  fidomtri  9922  prdom2  9935  cardaleph  10018  ackbij1lem16  10163  coflim  10190  coftr  10202  infpssrlem4  10235  isfin7-2  10325  axdc3lem2  10380  axdc3lem4  10382  brdom6disj  10461  entric  10486  fpwwe2lem11  10570  inatsk  10707  grur1a  10748  indpi  10836  reclem3pr  10978  supsrlem  11040  lelttr  11240  dedekindle  11314  negn0  11583  fimaxre  12103  fiminre  12106  nnmulcl  12186  arch  12415  nnnegz  12508  zle0orge1  12522  zeo  12596  uzm1  12807  rpneg  12961  xrlttri  13075  xrlelttr  13092  iccid  13327  icoshft  13410  fzen  13478  elfz1b  13530  fzdif1  13542  elfz2nn0  13555  fzoopth  13699  fleqceilz  13792  zmodidfzoimp  13839  modsumfzodifsn  13885  hasheqf1oi  14292  hashnfinnn0  14302  hashle2prv  14419  swrd0  14599  pfxccatin12lem2  14672  swrdccat  14676  swrdccat3blem  14680  repswswrd  14725  trclublem  14937  max0add  15252  abslt  15257  absle  15258  rexuzre  15295  caurcvg  15619  caucvg  15621  dvdsval2  16201  negdvdsb  16218  muldvds2  16227  dvdsabseq  16259  smuval2  16428  smupvallem  16429  rplpwr  16504  alginv  16521  algfx  16526  coprmgcdb  16595  divgcdcoprm0  16611  oddprmgt2  16645  rpexp1i  16669  qnumdencl  16685  phiprmpw  16722  prmdiveq  16732  prm23lt5  16761  pcmpt  16839  infpnlem1  16857  prmgaplem3  17000  prmgaplem8  17005  imasaddfnlem  17467  plelttr  18283  lubval  18295  lublecllem  18299  glbval  18308  mndind  18737  mndodconglem  19455  sdrgacs  20721  xrge0omnd  21387  elfrlmbasn0  21705  mavmulsolcl  22471  slesolex  22602  fvmptnn04if  22769  chfacfisf  22774  chfacfisfcpmat  22775  cnpnei  23184  unconn  23349  comppfsc  23452  kqsat  23651  isr0  23657  qtophmeo  23737  trufil  23830  alexsubALT  23971  cnextcn  23987  ucnima  24201  iducn  24203  bl2in  24321  addcnlem  24786  rescncf  24823  ovoliunlem2  25437  voliun  25488  mbflimsup  25600  itgcn  25779  dvdsq1p  26101  aalioulem2  26274  recosf1o  26477  logrec  26706  xrlimcnp  26911  basellem4  27027  bposlem1  27228  bposlem5  27232  lgsqrmod  27296  lgsdchrval  27298  2lgslem1a1  27333  pntlem3  27553  nosupbnd1  27659  noinfbnd1  27674  oldbday  27850  lrcut  27853  absslt  28191  zsoring  28336  brbtwn2  28885  axbtwnid  28919  elntg2  28965  umgredgprv  29087  umgrpredgv  29120  usgredgprvALT  29175  fusgrfisstep  29309  fusgrfis  29310  nbupgr  29324  nbumgrvtx  29326  finsumvtxdg2size  29531  wlkp1lem8  29659  upgr2pthnlp  29712  wwlksnextinj  29879  usgr2wspthons3  29944  clwwlkccatlem  29968  clwlkclwwlklem2a1  29971  clwwisshclwws  29994  wwlksext2clwwlk  30036  clwwlknonex2lem2  30087  eucrctshift  30222  eucrct2eupth  30224  numclwwlk2lem1  30355  numclwwlk5lem  30366  frgrreggt1  30372  frgrreg  30373  friendship  30378  blocn2  30787  htthlem  30896  axhcompl-zf  30977  spanuni  31523  spansncol  31547  spansneleq  31549  elspansn5  31553  idcnop  31960  pjnormssi  32147  dmdmd  32279  bian1dOLD  32436  n0nsnel  32494  ifeqeqx  32521  opabssi  32591  ac6mapd  32599  ressupprn  32663  supxrnemnf  32741  rexdiv  32896  xrstos  32994  cnre2csqlem  33893  fsumcvg4  33933  lmxrge0  33935  qqhval2lem  33964  esumpr2  34050  esumcvg  34069  issgon  34106  measxun2  34193  measres  34205  measdivcst  34207  measdivcstALTV  34208  elorrvc  34448  signsply0  34535  bnj580  34896  nummin  35074  0nn0m1nnn0  35093  umgracycusgr  35134  erdsze2lem2  35184  cvmsval  35246  fmlasuc  35366  fundmpss  35747  dfon2lem3  35766  dfrdg4  35932  cgrtriv  35983  btwntriv2  35993  ifscgr  36025  lineext  36057  btwnconn1lem12  36079  colinbtwnle  36099  elicc3  36298  ontgval  36412  onsucconni  36418  bj-bibibi  36567  bj-cbval  36630  bj-cbvex  36631  bj-cbvexw  36657  bj-equsal  36807  bj-gabeqd  36918  bj-restn0  37071  bj-snmoore  37094  bj-elsn0  37136  bj-finsumval0  37266  relowlssretop  37344  sucneqond  37346  finxpsuc  37379  pibt2  37398  wl-nfs1t  37518  finixpnum  37592  ltflcei  37595  matunitlindflem1  37603  poimirlem23  37630  poimirlem24  37631  poimirlem27  37634  poimirlem32  37639  itg2addnclem  37658  areacirclem2  37696  areacirclem5  37699  areacirc  37700  nninfnub  37738  prdstotbnd  37781  heiborlem4  37801  heibor  37808  elghomlem2OLD  37873  grpokerinj  37880  isidlc  38002  disjlem17  38784  prtlem17  38862  dral1-o  38890  axc16g-o  38920  lsator0sp  38987  atlrelat1  39307  cvratlem  39408  diaintclN  41045  dibintclN  41154  cdlemn11pre  41197  dihord2pre  41212  dihintcl  41331  dochkrshp4  41376  lcfrlem9  41537  lcfrlem21  41550  mapdh8e  41771  aks4d1p5  42061  aks6d1c1p1  42088  sticksstones4  42130  0prjspnrel  42608  elrfirn2  42677  rencldnfilem  42801  onsupnmax  43210  onov0suclim  43256  oege1  43288  cantnfresb  43306  dflim5  43311  omabs2  43314  refimssco  43589  rtrclex  43599  intimasn  43639  ss2iundf  43641  ov2ssiunov2  43682  comptiunov2i  43688  iunrelexpuztr  43701  dssmapf1od  44003  mnringmulrcld  44210  mnuprdlem1  44254  mnuprdlem2  44255  snelpwrVD  44813  en3lplem1VD  44825  en3lpVD  44827  orbi1rVD  44830  sbc3orgVD  44833  3impexpVD  44838  equncomVD  44850  trsbcVD  44859  trintALTVD  44862  trintALT  44863  csbingVD  44866  csbsngVD  44875  csbxpgVD  44876  csbrngVD  44878  csbfv12gALTVD  44881  relopabVD  44883  e2ebindVD  44894  xlimpnfxnegmnf  45805  xlimbr  45818  stoweidlem35  46026  stoweidlem48  46039  ormkglobd  46866  cjnpoly  46883  tannpoly  46884  n0nsn2el  47019  rexrsb  47094  2reu8i  47107  funbrafv  47152  rlimdmafv  47171  tz6.12c-afv2  47236  rlimdmafv2  47252  fzopredsuc  47317  2ffzoeq  47321  m1modnep2mod  47346  eqfvelsetpreimafv  47387  iccpartlt  47418  proththd  47608  even3prm2  47713  fppr2odd  47725  sbgoldbm  47778  nnsum3primesle9  47788  wtgoldbnnsum4prm  47796  bgoldbnnsum3prm  47798  grtrif1o  47934  mgm2mgm  48208  2zrngnmlid  48236  2zrngnmrid  48237  ellcoellss  48417  nneop  48508  fldivexpfllog2  48547  digexp  48589  reorelicc  48692  2itscp  48763  oppc1stflem  49269  prsthinc  49446  elpglem2  49694