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  342  biimpar  479  prlem1  1054  alexbii  1836  speivw  1978  spfw  2037  cbvalw  2039  alcomiw  2047  cbvalv1  2338  cbval  2398  axc16i  2436  sb3  2477  sb2  2479  axc16gALT  2490  eqrdav  2732  ralbida  3268  rspcimdv  3603  rspcedv  3606  moi2  3713  moi  3715  sspsstr  4106  2nreu  4442  rabsnifsb  4727  ralxfr2d  5409  axprlem4  5425  sbcop1  5489  isso2i  5624  wefrc  5671  elinxp  6020  sotri3  6132  oneqmini  6417  ordsssuc2  6456  ordtri2or  6463  iotan0  6534  2elresin  6672  f1ocnv  6846  tz6.12cOLD  6919  fveqres  6939  fvun1  6983  dffo4  7105  funopsn  7146  fconst5  7207  fnprb  7210  fntpb  7211  isores3  7332  f1owe  7350  weniso  7351  ndmovordi  7598  abnexg  7743  ordsuc  7801  orduniorsuc  7818  ordzsl  7834  tfinds  7849  dmfexALT  7901  f1oweALT  7959  opreuopreu  8020  fnse  8119  poxp3  8136  poseq  8144  soseq  8145  tposfo2  8234  fprlem1  8285  wfrlem5OLD  8313  wfrlem12OLD  8320  issmo2  8349  iordsmo  8357  smoel2  8363  tz7.48lem  8441  oawordeulem  8554  om00  8575  omlimcl  8578  odi  8579  nnawordi  8621  unfi  9172  php2  9211  fiint  9324  fipreima  9358  dffi2  9418  suplub2  9456  wemapsolem  9545  unwdomg  9579  inf3lem3  9625  trcl  9723  frrlem15  9752  fidomtri  9988  prdom2  10001  cardaleph  10084  ackbij1lem16  10230  coflim  10256  coftr  10268  infpssrlem4  10301  isfin7-2  10391  axdc3lem2  10446  axdc3lem4  10448  brdom6disj  10527  entric  10552  fpwwe2lem11  10636  inatsk  10773  grur1a  10814  indpi  10902  reclem3pr  11044  supsrlem  11106  lelttr  11304  dedekindle  11378  negn0  11643  fimaxre  12158  fiminre  12161  nnmulcl  12236  arch  12469  nnnegz  12561  zle0orge1  12575  zeo  12648  uzm1  12860  rpneg  13006  xrlttri  13118  xrlelttr  13135  iccid  13369  icoshft  13450  fzen  13518  elfz1b  13570  elfz2nn0  13592  fleqceilz  13819  zmodidfzoimp  13866  modsumfzodifsn  13909  hasheqf1oi  14311  hashnfinnn0  14321  hashle2prv  14439  swrd0  14608  pfxccatin12lem2  14681  swrdccat  14685  swrdccat3blem  14689  repswswrd  14734  trclublem  14942  max0add  15257  abslt  15261  absle  15262  rexuzre  15299  caurcvg  15623  caucvg  15625  dvdsval2  16200  negdvdsb  16216  muldvds2  16225  dvdsabseq  16256  smuval2  16423  smupvallem  16424  rplpwr  16499  alginv  16512  algfx  16517  coprmgcdb  16586  divgcdcoprm0  16602  oddprmgt2  16636  rpexp1i  16660  qnumdencl  16675  phiprmpw  16709  prmdiveq  16719  prm23lt5  16747  pcmpt  16825  infpnlem1  16843  prmgaplem3  16986  prmgaplem8  16991  imasaddfnlem  17474  plelttr  18297  lubval  18309  lublecllem  18313  glbval  18322  mndind  18709  mndodconglem  19409  sdrgacs  20417  elfrlmbasn0  21318  mavmulsolcl  22053  slesolex  22184  fvmptnn04if  22351  chfacfisf  22356  chfacfisfcpmat  22357  cnpnei  22768  unconn  22933  comppfsc  23036  kqsat  23235  isr0  23241  qtophmeo  23321  trufil  23414  alexsubALT  23555  cnextcn  23571  ucnima  23786  iducn  23788  bl2in  23906  addcnlem  24380  rescncf  24413  ovoliunlem2  25020  voliun  25071  mbflimsup  25183  itgcn  25362  dvdsq1p  25678  aalioulem2  25846  recosf1o  26044  logrec  26268  xrlimcnp  26473  basellem4  26588  bposlem1  26787  bposlem5  26791  lgsqrmod  26855  lgsdchrval  26857  2lgslem1a1  26892  pntlem3  27112  nosupbnd1  27217  noinfbnd1  27232  oldbday  27395  lrcut  27397  brbtwn2  28163  axbtwnid  28197  elntg2  28243  umgredgprv  28367  umgrpredgv  28400  usgredgprvALT  28452  fusgrfisstep  28586  fusgrfis  28587  nbupgr  28601  nbumgrvtx  28603  finsumvtxdg2size  28807  wlkp1lem8  28937  upgr2pthnlp  28989  wwlksnextinj  29153  usgr2wspthons3  29218  clwwlkccatlem  29242  clwlkclwwlklem2a1  29245  clwwisshclwws  29268  wwlksext2clwwlk  29310  clwwlknonex2lem2  29361  eucrctshift  29496  eucrct2eupth  29498  numclwwlk2lem1  29629  numclwwlk5lem  29640  frgrreggt1  29646  frgrreg  29647  friendship  29652  blocn2  30061  htthlem  30170  axhcompl-zf  30251  spanuni  30797  spansncol  30821  spansneleq  30823  elspansn5  30827  idcnop  31234  pjnormssi  31421  dmdmd  31553  bian1d  31700  ifeqeqx  31774  opabssi  31842  ressupprn  31912  supxrnemnf  31981  rexdiv  32092  xrstos  32180  xrge0omnd  32229  cnre2csqlem  32890  fsumcvg4  32930  lmxrge0  32932  qqhval2lem  32961  esumpr2  33065  esumcvg  33084  issgon  33121  measxun2  33208  measres  33220  measdivcst  33222  measdivcstALTV  33223  elorrvc  33462  signsply0  33562  bnj580  33924  nummin  34094  0nn0m1nnn0  34102  umgracycusgr  34145  erdsze2lem2  34195  cvmsval  34257  fmlasuc  34377  fundmpss  34738  dfon2lem3  34757  dfrdg4  34923  cgrtriv  34974  btwntriv2  34984  ifscgr  35016  lineext  35048  btwnconn1lem12  35070  colinbtwnle  35090  elicc3  35202  ontgval  35316  onsucconni  35322  bj-bibibi  35464  bj-cbval  35526  bj-cbvex  35527  bj-cbvexw  35553  bj-equsal  35704  bj-gabeqd  35817  bj-restn0  35971  bj-snmoore  35994  bj-elsn0  36036  bj-finsumval0  36166  relowlssretop  36244  sucneqond  36246  finxpsuc  36279  pibt2  36298  wl-nfs1t  36406  finixpnum  36473  ltflcei  36476  matunitlindflem1  36484  poimirlem23  36511  poimirlem24  36512  poimirlem27  36515  poimirlem32  36520  itg2addnclem  36539  areacirclem2  36577  areacirclem5  36580  areacirc  36581  nninfnub  36619  prdstotbnd  36662  heiborlem4  36682  heibor  36689  elghomlem2OLD  36754  grpokerinj  36761  isidlc  36883  disjlem17  37669  prtlem17  37746  dral1-o  37774  axc16g-o  37804  lsator0sp  37871  atlrelat1  38191  cvratlem  38292  diaintclN  39929  dibintclN  40038  cdlemn11pre  40081  dihord2pre  40096  dihintcl  40215  dochkrshp4  40260  lcfrlem9  40421  lcfrlem21  40434  mapdh8e  40655  aks4d1p5  40945  sticksstones4  40965  metakunt29  41013  0prjspnrel  41369  elrfirn2  41434  rencldnfilem  41558  onsupnmax  41977  onov0suclim  42024  oege1  42056  cantnfresb  42074  dflim5  42079  omabs2  42082  refimssco  42358  rtrclex  42368  intimasn  42408  ss2iundf  42410  ov2ssiunov2  42451  comptiunov2i  42457  iunrelexpuztr  42470  dssmapf1od  42772  mnringmulrcld  42987  mnuprdlem1  43031  mnuprdlem2  43032  snelpwrVD  43592  en3lplem1VD  43604  en3lpVD  43606  orbi1rVD  43609  sbc3orgVD  43612  3impexpVD  43617  equncomVD  43629  trsbcVD  43638  trintALTVD  43641  trintALT  43642  csbingVD  43645  csbsngVD  43654  csbxpgVD  43655  csbrngVD  43657  csbfv12gALTVD  43660  relopabVD  43662  e2ebindVD  43673  xlimpnfxnegmnf  44530  xlimbr  44543  stoweidlem35  44751  stoweidlem48  44764  n0nsn2el  45735  rexrsb  45808  2reu8i  45821  funbrafv  45866  rlimdmafv  45885  tz6.12c-afv2  45950  rlimdmafv2  45966  fzopredsuc  46031  fzoopth  46035  2ffzoeq  46036  eqfvelsetpreimafv  46061  iccpartlt  46092  proththd  46282  even3prm2  46387  fppr2odd  46399  sbgoldbm  46452  nnsum3primesle9  46462  wtgoldbnnsum4prm  46470  bgoldbnnsum3prm  46472  mgm2mgm  46637  2zrngnmlid  46847  2zrngnmrid  46848  ellcoellss  47116  nneop  47212  fldivexpfllog2  47251  digexp  47293  reorelicc  47396  2itscp  47467  prsthinc  47674  elpglem2  47757