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  253  mpbird  256  sylibrd  258  sylbird  259  con4bid  316  mtbid  323  mtbii  325  imbi1d  341  biimpar  478  prlem1  1053  alexbii  1835  speivw  1977  spfw  2036  cbvalw  2038  alcomiw  2046  cbvalv1  2337  cbval  2396  axc16i  2434  sb3  2475  sb2  2477  axc16gALT  2488  eqrdav  2730  ralbida  3251  rspcimdv  3572  rspcedv  3575  moi2  3677  moi  3679  sspsstr  4070  2nreu  4406  rabsnifsb  4688  ralxfr2d  5370  axprlem4  5386  sbcop1  5450  isso2i  5585  wefrc  5632  elinxp  5980  sotri3  6089  oneqmini  6374  ordsssuc2  6413  ordtri2or  6420  iotan0  6491  2elresin  6627  f1ocnv  6801  tz6.12cOLD  6874  fveqres  6894  fvun1  6937  dffo4  7058  funopsn  7099  fconst5  7160  fnprb  7163  fntpb  7164  isores3  7285  f1owe  7303  weniso  7304  ndmovordi  7550  abnexg  7695  ordsuc  7753  orduniorsuc  7770  ordzsl  7786  tfinds  7801  dmfexALT  7852  f1oweALT  7910  opreuopreu  7971  fnse  8070  poxp3  8087  poseq  8095  soseq  8096  tposfo2  8185  fprlem1  8236  wfrlem5OLD  8264  wfrlem12OLD  8271  issmo2  8300  iordsmo  8308  smoel2  8314  tz7.48lem  8392  oawordeulem  8506  om00  8527  omlimcl  8530  odi  8531  nnawordi  8573  unfi  9123  php2  9162  fiint  9275  fipreima  9309  dffi2  9368  suplub2  9406  wemapsolem  9495  unwdomg  9529  inf3lem3  9575  trcl  9673  frrlem15  9702  fidomtri  9938  prdom2  9951  cardaleph  10034  ackbij1lem16  10180  coflim  10206  coftr  10218  infpssrlem4  10251  isfin7-2  10341  axdc3lem2  10396  axdc3lem4  10398  brdom6disj  10477  entric  10502  fpwwe2lem11  10586  inatsk  10723  grur1a  10764  indpi  10852  reclem3pr  10994  supsrlem  11056  lelttr  11254  dedekindle  11328  negn0  11593  fimaxre  12108  fiminre  12111  nnmulcl  12186  arch  12419  nnnegz  12511  zle0orge1  12525  zeo  12598  uzm1  12810  rpneg  12956  xrlttri  13068  xrlelttr  13085  iccid  13319  icoshft  13400  fzen  13468  elfz1b  13520  elfz2nn0  13542  fleqceilz  13769  zmodidfzoimp  13816  modsumfzodifsn  13859  hasheqf1oi  14261  hashnfinnn0  14271  hashle2prv  14389  swrd0  14558  pfxccatin12lem2  14631  swrdccat  14635  swrdccat3blem  14639  repswswrd  14684  trclublem  14892  max0add  15207  abslt  15211  absle  15212  rexuzre  15249  caurcvg  15573  caucvg  15575  dvdsval2  16150  negdvdsb  16166  muldvds2  16175  dvdsabseq  16206  smuval2  16373  smupvallem  16374  rplpwr  16449  alginv  16462  algfx  16467  coprmgcdb  16536  divgcdcoprm0  16552  oddprmgt2  16586  rpexp1i  16610  qnumdencl  16625  phiprmpw  16659  prmdiveq  16669  prm23lt5  16697  pcmpt  16775  infpnlem1  16793  prmgaplem3  16936  prmgaplem8  16941  imasaddfnlem  17424  plelttr  18247  lubval  18259  lublecllem  18263  glbval  18272  mndind  18652  mndodconglem  19337  sdrgacs  20324  elfrlmbasn0  21206  mavmulsolcl  21937  slesolex  22068  fvmptnn04if  22235  chfacfisf  22240  chfacfisfcpmat  22241  cnpnei  22652  unconn  22817  comppfsc  22920  kqsat  23119  isr0  23125  qtophmeo  23205  trufil  23298  alexsubALT  23439  cnextcn  23455  ucnima  23670  iducn  23672  bl2in  23790  addcnlem  24264  rescncf  24297  ovoliunlem2  24904  voliun  24955  mbflimsup  25067  itgcn  25246  dvdsq1p  25562  aalioulem2  25730  recosf1o  25928  logrec  26150  xrlimcnp  26355  basellem4  26470  bposlem1  26669  bposlem5  26673  lgsqrmod  26737  lgsdchrval  26739  2lgslem1a1  26774  pntlem3  26994  nosupbnd1  27099  noinfbnd1  27114  oldbday  27273  lrcut  27275  brbtwn2  27917  axbtwnid  27951  elntg2  27997  umgredgprv  28121  umgrpredgv  28154  usgredgprvALT  28206  fusgrfisstep  28340  fusgrfis  28341  nbupgr  28355  nbumgrvtx  28357  finsumvtxdg2size  28561  wlkp1lem8  28691  upgr2pthnlp  28743  wwlksnextinj  28907  usgr2wspthons3  28972  clwwlkccatlem  28996  clwlkclwwlklem2a1  28999  clwwisshclwws  29022  wwlksext2clwwlk  29064  clwwlknonex2lem2  29115  eucrctshift  29250  eucrct2eupth  29252  numclwwlk2lem1  29383  numclwwlk5lem  29394  frgrreggt1  29400  frgrreg  29401  friendship  29406  blocn2  29813  htthlem  29922  axhcompl-zf  30003  spanuni  30549  spansncol  30573  spansneleq  30575  elspansn5  30579  idcnop  30986  pjnormssi  31173  dmdmd  31305  bian1d  31452  ifeqeqx  31528  opabssi  31599  ressupprn  31672  supxrnemnf  31741  rexdiv  31852  xrstos  31940  xrge0omnd  31989  cnre2csqlem  32580  fsumcvg4  32620  lmxrge0  32622  qqhval2lem  32651  esumpr2  32755  esumcvg  32774  issgon  32811  measxun2  32898  measres  32910  measdivcst  32912  measdivcstALTV  32913  elorrvc  33152  signsply0  33252  bnj580  33614  nummin  33784  0nn0m1nnn0  33792  umgracycusgr  33835  erdsze2lem2  33885  cvmsval  33947  fmlasuc  34067  fundmpss  34427  dfon2lem3  34446  dfrdg4  34612  cgrtriv  34663  btwntriv2  34673  ifscgr  34705  lineext  34737  btwnconn1lem12  34759  colinbtwnle  34779  elicc3  34865  ontgval  34979  onsucconni  34985  bj-bibibi  35127  bj-cbval  35189  bj-cbvex  35190  bj-cbvexw  35216  bj-equsal  35367  bj-gabeqd  35480  bj-restn0  35634  bj-snmoore  35657  bj-elsn0  35699  bj-finsumval0  35829  relowlssretop  35907  sucneqond  35909  finxpsuc  35942  pibt2  35961  wl-nfs1t  36069  finixpnum  36136  ltflcei  36139  matunitlindflem1  36147  poimirlem23  36174  poimirlem24  36175  poimirlem27  36178  poimirlem32  36183  itg2addnclem  36202  areacirclem2  36240  areacirclem5  36243  areacirc  36244  nninfnub  36283  prdstotbnd  36326  heiborlem4  36346  heibor  36353  elghomlem2OLD  36418  grpokerinj  36425  isidlc  36547  disjlem17  37334  prtlem17  37411  dral1-o  37439  axc16g-o  37469  lsator0sp  37536  atlrelat1  37856  cvratlem  37957  diaintclN  39594  dibintclN  39703  cdlemn11pre  39746  dihord2pre  39761  dihintcl  39880  dochkrshp4  39925  lcfrlem9  40086  lcfrlem21  40099  mapdh8e  40320  aks4d1p5  40610  sticksstones4  40630  metakunt29  40678  0prjspnrel  41023  elrfirn2  41077  rencldnfilem  41201  onsupnmax  41620  onov0suclim  41667  oege1  41699  cantnfresb  41717  dflim5  41722  omabs2  41725  refimssco  42001  rtrclex  42011  intimasn  42051  ss2iundf  42053  ov2ssiunov2  42094  comptiunov2i  42100  iunrelexpuztr  42113  dssmapf1od  42415  mnringmulrcld  42630  mnuprdlem1  42674  mnuprdlem2  42675  snelpwrVD  43235  en3lplem1VD  43247  en3lpVD  43249  orbi1rVD  43252  sbc3orgVD  43255  3impexpVD  43260  equncomVD  43272  trsbcVD  43281  trintALTVD  43284  trintALT  43285  csbingVD  43288  csbsngVD  43297  csbxpgVD  43298  csbrngVD  43300  csbfv12gALTVD  43303  relopabVD  43305  e2ebindVD  43316  xlimpnfxnegmnf  44175  xlimbr  44188  stoweidlem35  44396  stoweidlem48  44409  rexrsb  45452  2reu8i  45465  funbrafv  45510  rlimdmafv  45529  tz6.12c-afv2  45594  rlimdmafv2  45610  fzopredsuc  45675  fzoopth  45679  2ffzoeq  45680  eqfvelsetpreimafv  45705  iccpartlt  45736  proththd  45926  even3prm2  46031  fppr2odd  46043  sbgoldbm  46096  nnsum3primesle9  46106  wtgoldbnnsum4prm  46114  bgoldbnnsum3prm  46116  mgm2mgm  46281  2zrngnmlid  46367  2zrngnmrid  46368  ellcoellss  46636  nneop  46732  fldivexpfllog2  46771  digexp  46813  reorelicc  46916  2itscp  46987  prsthinc  47194  elpglem2  47277