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	imbitrrid 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  254  mpbird  257  sylibrd  259  sylbird  260  con4bid  317  mtbid  324  mtbii  326  imbi1d  341  biimpar  477  prlem1  1052  alexbii  1834  speivw  1976  spfw  2035  cbvalw  2037  alcomiw  2045  cbvalv1  2336  cbval  2396  axc16i  2434  sb3  2475  sb2  2477  axc16gALT  2488  eqrdav  2730  ralbida  3266  rspcimdv  3602  rspcedv  3605  moi2  3712  moi  3714  sspsstr  4105  2nreu  4441  rabsnifsb  4726  ralxfr2d  5408  axprlem4  5424  sbcop1  5488  isso2i  5623  wefrc  5670  elinxp  6019  sotri3  6131  oneqmini  6416  ordsssuc2  6455  ordtri2or  6462  iotan0  6533  2elresin  6671  f1ocnv  6845  tz6.12cOLD  6918  fveqres  6938  fvun1  6982  dffo4  7104  funopsn  7148  fconst5  7209  fnprb  7212  fntpb  7213  isores3  7335  f1owe  7353  weniso  7354  ndmovordi  7602  abnexg  7747  ordsuc  7805  orduniorsuc  7822  ordzsl  7838  tfinds  7853  dmfexALT  7905  f1oweALT  7963  opreuopreu  8024  fnse  8124  poxp3  8141  poseq  8149  soseq  8150  tposfo2  8240  fprlem1  8291  wfrlem5OLD  8319  wfrlem12OLD  8326  issmo2  8355  iordsmo  8363  smoel2  8369  tz7.48lem  8447  oawordeulem  8560  om00  8581  omlimcl  8584  odi  8585  nnawordi  8627  unfi  9178  php2  9217  fiint  9330  fipreima  9364  dffi2  9424  suplub2  9462  wemapsolem  9551  unwdomg  9585  inf3lem3  9631  trcl  9729  frrlem15  9758  fidomtri  9994  prdom2  10007  cardaleph  10090  ackbij1lem16  10236  coflim  10262  coftr  10274  infpssrlem4  10307  isfin7-2  10397  axdc3lem2  10452  axdc3lem4  10454  brdom6disj  10533  entric  10558  fpwwe2lem11  10642  inatsk  10779  grur1a  10820  indpi  10908  reclem3pr  11050  supsrlem  11112  lelttr  11311  dedekindle  11385  negn0  11650  fimaxre  12165  fiminre  12168  nnmulcl  12243  arch  12476  nnnegz  12568  zle0orge1  12582  zeo  12655  uzm1  12867  rpneg  13013  xrlttri  13125  xrlelttr  13142  iccid  13376  icoshft  13457  fzen  13525  elfz1b  13577  elfz2nn0  13599  fleqceilz  13826  zmodidfzoimp  13873  modsumfzodifsn  13916  hasheqf1oi  14318  hashnfinnn0  14328  hashle2prv  14446  swrd0  14615  pfxccatin12lem2  14688  swrdccat  14692  swrdccat3blem  14696  repswswrd  14741  trclublem  14949  max0add  15264  abslt  15268  absle  15269  rexuzre  15306  caurcvg  15630  caucvg  15632  dvdsval2  16207  negdvdsb  16223  muldvds2  16232  dvdsabseq  16263  smuval2  16430  smupvallem  16431  rplpwr  16506  alginv  16519  algfx  16524  coprmgcdb  16593  divgcdcoprm0  16609  oddprmgt2  16643  rpexp1i  16667  qnumdencl  16682  phiprmpw  16716  prmdiveq  16726  prm23lt5  16754  pcmpt  16832  infpnlem1  16850  prmgaplem3  16993  prmgaplem8  16998  imasaddfnlem  17481  plelttr  18307  lubval  18319  lublecllem  18323  glbval  18332  mndind  18751  mndodconglem  19457  sdrgacs  20648  elfrlmbasn0  21628  mavmulsolcl  22373  slesolex  22504  fvmptnn04if  22671  chfacfisf  22676  chfacfisfcpmat  22677  cnpnei  23088  unconn  23253  comppfsc  23356  kqsat  23555  isr0  23561  qtophmeo  23641  trufil  23734  alexsubALT  23875  cnextcn  23891  ucnima  24106  iducn  24108  bl2in  24226  addcnlem  24700  rescncf  24737  ovoliunlem2  25352  voliun  25403  mbflimsup  25515  itgcn  25694  dvdsq1p  26016  aalioulem2  26185  recosf1o  26384  logrec  26609  xrlimcnp  26814  basellem4  26930  bposlem1  27131  bposlem5  27135  lgsqrmod  27199  lgsdchrval  27201  2lgslem1a1  27236  pntlem3  27456  nosupbnd1  27561  noinfbnd1  27576  oldbday  27741  lrcut  27743  absslt  28057  brbtwn2  28597  axbtwnid  28631  elntg2  28677  umgredgprv  28801  umgrpredgv  28834  usgredgprvALT  28886  fusgrfisstep  29020  fusgrfis  29021  nbupgr  29035  nbumgrvtx  29037  finsumvtxdg2size  29241  wlkp1lem8  29371  upgr2pthnlp  29423  wwlksnextinj  29587  usgr2wspthons3  29652  clwwlkccatlem  29676  clwlkclwwlklem2a1  29679  clwwisshclwws  29702  wwlksext2clwwlk  29744  clwwlknonex2lem2  29795  eucrctshift  29930  eucrct2eupth  29932  numclwwlk2lem1  30063  numclwwlk5lem  30074  frgrreggt1  30080  frgrreg  30081  friendship  30086  blocn2  30495  htthlem  30604  axhcompl-zf  30685  spanuni  31231  spansncol  31255  spansneleq  31257  elspansn5  31261  idcnop  31668  pjnormssi  31855  dmdmd  31987  bian1d  32134  ifeqeqx  32208  opabssi  32276  ressupprn  32346  supxrnemnf  32415  rexdiv  32526  xrstos  32614  xrge0omnd  32666  cnre2csqlem  33355  fsumcvg4  33395  lmxrge0  33397  qqhval2lem  33426  esumpr2  33530  esumcvg  33549  issgon  33586  measxun2  33673  measres  33685  measdivcst  33687  measdivcstALTV  33688  elorrvc  33927  signsply0  34027  bnj580  34389  nummin  34559  0nn0m1nnn0  34567  umgracycusgr  34610  erdsze2lem2  34660  cvmsval  34722  fmlasuc  34842  fundmpss  35209  dfon2lem3  35228  dfrdg4  35394  cgrtriv  35445  btwntriv2  35455  ifscgr  35487  lineext  35519  btwnconn1lem12  35541  colinbtwnle  35561  elicc3  35668  ontgval  35782  onsucconni  35788  bj-bibibi  35930  bj-cbval  35992  bj-cbvex  35993  bj-cbvexw  36019  bj-equsal  36170  bj-gabeqd  36283  bj-restn0  36437  bj-snmoore  36460  bj-elsn0  36502  bj-finsumval0  36632  relowlssretop  36710  sucneqond  36712  finxpsuc  36745  pibt2  36764  wl-nfs1t  36872  finixpnum  36939  ltflcei  36942  matunitlindflem1  36950  poimirlem23  36977  poimirlem24  36978  poimirlem27  36981  poimirlem32  36986  itg2addnclem  37005  areacirclem2  37043  areacirclem5  37046  areacirc  37047  nninfnub  37085  prdstotbnd  37128  heiborlem4  37148  heibor  37155  elghomlem2OLD  37220  grpokerinj  37227  isidlc  37349  disjlem17  38135  prtlem17  38212  dral1-o  38240  axc16g-o  38270  lsator0sp  38337  atlrelat1  38657  cvratlem  38758  diaintclN  40395  dibintclN  40504  cdlemn11pre  40547  dihord2pre  40562  dihintcl  40681  dochkrshp4  40726  lcfrlem9  40887  lcfrlem21  40900  mapdh8e  41121  aks4d1p5  41414  sticksstones4  41434  metakunt29  41482  0prjspnrel  41834  elrfirn2  41899  rencldnfilem  42023  onsupnmax  42442  onov0suclim  42489  oege1  42521  cantnfresb  42539  dflim5  42544  omabs2  42547  refimssco  42823  rtrclex  42833  intimasn  42873  ss2iundf  42875  ov2ssiunov2  42916  comptiunov2i  42922  iunrelexpuztr  42935  dssmapf1od  43237  mnringmulrcld  43452  mnuprdlem1  43496  mnuprdlem2  43497  snelpwrVD  44057  en3lplem1VD  44069  en3lpVD  44071  orbi1rVD  44074  sbc3orgVD  44077  3impexpVD  44082  equncomVD  44094  trsbcVD  44103  trintALTVD  44106  trintALT  44107  csbingVD  44110  csbsngVD  44119  csbxpgVD  44120  csbrngVD  44122  csbfv12gALTVD  44125  relopabVD  44127  e2ebindVD  44138  xlimpnfxnegmnf  44991  xlimbr  45004  stoweidlem35  45212  stoweidlem48  45225  n0nsn2el  46196  rexrsb  46269  2reu8i  46282  funbrafv  46327  rlimdmafv  46346  tz6.12c-afv2  46411  rlimdmafv2  46427  fzopredsuc  46492  fzoopth  46496  2ffzoeq  46497  eqfvelsetpreimafv  46522  iccpartlt  46553  proththd  46743  even3prm2  46848  fppr2odd  46860  sbgoldbm  46913  nnsum3primesle9  46923  wtgoldbnnsum4prm  46931  bgoldbnnsum3prm  46933  mgm2mgm  47066  2zrngnmlid  47094  2zrngnmrid  47095  ellcoellss  47280  nneop  47376  fldivexpfllog2  47415  digexp  47457  reorelicc  47560  2itscp  47631  prsthinc  47838  elpglem2  47921