Theorem biimprd 237

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

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  syl6bir  243  mpbird  246  sylibrd  248  sylbird  249  con4bid  306  mtbid  313  mtbii  315  imbi1d  330  biimpar  501  prlem1  997  alexbii  1750  spfw  1952  spfwOLD  1953  cbvalw  1955  alcomiw  1958  axc11nlemOLD2  1975  ax12vOLDOLD  2038  axc11nlemOLD  2146  cbvalv1  2163  nfimdOLD  2214  cbval  2259  axc11nlemALT  2294  axc16i  2310  axc16gALT  2355  eqrdav  2609  pm13.18  2863  rspcimdv  3283  rspcedv  3286  moi2  3354  moi  3356  eqrd  3586  sspsstr  3674  eqoreldifOLD  4173  rabsnifsb  4201  ralxfrdOLD  4806  ralxfr2d  4808  isso2i  4991  wefrc  5032  elres  5355  sotri3  5445  oneqmini  5693  ordsssuc2  5731  ordtri2or  5739  2elresin  5916  f1ocnv  6062  tz6.12c  6123  fveqres  6140  fvun1  6179  dffo4  6283  funopsn  6319  fconst5  6376  fnprb  6377  fntpb  6378  isores3  6485  f1owe  6503  weniso  6504  ndmovordi  6723  orduniorsuc  6922  ordzsl  6937  tfinds  6951  f1oweALT  7043  fnse  7181  tposfo2  7262  wfrlem5  7306  wfrlem12  7313  issmo2  7333  iordsmo  7341  smoel2  7347  tz7.48lem  7423  oawordeulem  7521  om00  7542  omlimcl  7545  odi  7546  nnawordi  7588  fiint  8122  fipreima  8155  dffi2  8212  suplub2  8250  wemapsolem  8338  unwdomg  8372  inf3lem3  8410  trcl  8487  fidomtri  8702  prdom2  8712  cardaleph  8795  ackbij1lem16  8940  coflim  8966  coftr  8978  infpssrlem4  9011  isfin7-2  9101  axdc3lem2  9156  axdc3lem4  9158  brdom6disj  9235  entric  9258  fpwwe2lem12  9342  inatsk  9479  grur1a  9520  indpi  9608  reclem3pr  9750  supsrlem  9811  lelttr  10007  dedekindle  10080  negn0  10338  fimaxre  10847  nnmulcl  10920  arch  11166  nnnegz  11257  zeo  11339  uzm1  11594  rpneg  11739  xrlttri  11848  xrlelttr  11863  iccid  12091  icoshft  12165  fzen  12229  elfz2nn0  12300  elfzom1p1elfzo  12414  fleqceilz  12515  zmodidfzoimp  12562  modsumfzodifsn  12605  hasheqf1oi  13002  hasheqf1oiOLD  13003  hashnfinnn0  13013  swrd0  13286  swrdccatin12lem2  13340  swrdccat  13344  swrdccat3blem  13346  repswswrd  13382  trclublem  13582  max0add  13898  abslt  13902  absle  13903  rexuzre  13940  caurcvg  14255  caucvg  14257  dvdsval2  14824  negdvdsb  14836  muldvds2  14845  dvdsabseq  14873  smuval2  15042  smupvallem  15043  rplpwr  15114  alginv  15126  algfx  15131  coprmgcdb  15200  divgcdcoprm0  15217  prmgt1  15247  oddprmgt2  15249  rpexp1i  15271  qnumdencl  15285  phiprmpw  15319  prmdiveq  15329  prm23lt5  15357  pcmpt  15434  infpnlem1  15452  prmgaplem3  15595  prmgaplem8  15600  imasaddfnlem  16011  plelttr  16795  lubval  16807  lublecllem  16811  glbval  16820  mrcmndind  17189  mndodconglem  17783  elfrlmbasn0  19925  mavmulsolcl  20176  slesolex  20307  fvmptnn04if  20473  chfacfisf  20478  chfacfisfcpmat  20479  cnpnei  20878  uncon  21042  comppfsc  21145  kqsat  21344  isr0  21350  qtophmeo  21430  trufil  21524  alexsubALT  21665  cnextcn  21681  ucnima  21895  iducn  21897  bl2in  22015  addcnlem  22475  rescncf  22508  ovoliunlem2  23078  voliun  23129  mbflimsup  23239  itgcn  23415  dvdsq1p  23724  aalioulem2  23892  recosf1o  24085  logrec  24301  xrlimcnp  24495  basellem4  24610  bposlem1  24809  bposlem5  24813  lgsqrmod  24877  lgsdchrval  24879  2lgslem1a1  24914  pntlem3  25098  brbtwn2  25585  axbtwnid  25619  umgredgprv  25773  umgrpredgav  25813  usgraedgprv  25905  usgraedgrnv  25906  usgrafisinds  25942  iswlkg  26052  wwlkextinj  26258  isclwlkg  26283  clwlkisclwwlklem2a1  26307  clwwisshclww  26335  eupai  26494  numclwwlkovf2ex  26613  numclwwlk2lem1  26629  numclwwlk5lem  26638  frgrareggt1  26643  friendship  26649  blocn2  27047  htthlem  27158  axhcompl-zf  27239  spanuni  27787  spansncol  27811  spansneleq  27813  elspansn5  27817  idcnop  28224  pjnormssi  28411  dmdmd  28543  bian1d  28690  ifeqeqx  28745  supxrnemnf  28924  rexdiv  28965  xrstos  29010  xrge0omnd  29042  cnre2csqlem  29284  fsumcvg4  29324  lmxrge0  29326  qqhval2lem  29353  esumpr2  29456  esumcvg  29475  issgon  29513  measxun2  29600  measres  29612  measdivcstOLD  29614  measdivcst  29615  elorrvc  29852  signsply0  29954  bnj580  30237  erdsze2lem2  30440  cvmsval  30502  fundmpss  30910  dfon2lem3  30934  frmin  30983  poseq  30994  soseq  30995  frrlem5  31028  frrlem11  31036  nobndup  31099  nobnddown  31100  dfrdg4  31228  cgrtriv  31279  btwntriv2  31289  ifscgr  31321  lineext  31353  btwnconn1lem12  31375  colinbtwnle  31395  elicc3  31481  ontgval  31600  onsucconi  31606  bj-bibibi  31744  bj-cbvexw  31851  bj-equsal  32001  bj-restn0  32224  bj-xnex  32245  bj-elid  32262  bj-finsumval0  32324  relowlssretop  32387  sucneqond  32389  finxpsuc  32411  wl-nfs1t  32503  finixpnum  32564  ltflcei  32567  matunitlindflem1  32575  poimirlem23  32602  poimirlem24  32603  poimirlem27  32606  poimirlem32  32611  itg2addnclem  32631  areacirclem2  32671  areacirclem5  32674  areacirc  32675  nninfnub  32717  prdstotbnd  32763  heiborlem4  32783  heibor  32790  elghomlem2OLD  32855  grpokerinj  32862  isidlc  32984  prtlem17  33179  dral1-o  33207  axc16g-o  33237  lsator0sp  33306  atlrelat1  33626  cvratlem  33725  diaintclN  35365  dibintclN  35474  cdlemn11pre  35517  dihord2pre  35532  dihintcl  35651  dochkrshp4  35696  lcfrlem9  35857  lcfrlem21  35870  mapdh8e  36091  elrfirn2  36277  rencldnfilem  36402  sdrgacs  36790  refimssco  36932  rtrclex  36943  intimasn  36968  ss2iundf  36970  ov2ssiunov2  37011  comptiunov2i  37017  iunrelexpuztr  37030  dssmapf1od  37335  snelpwrVD  38088  en3lplem1VD  38100  en3lpVD  38102  orbi1rVD  38105  sbc3orgVD  38108  3impexpVD  38113  equncomVD  38126  trsbcVD  38135  trintALTVD  38138  trintALT  38139  csbingVD  38142  csbsngVD  38151  csbxpgVD  38152  csbrngVD  38154  csbfv12gALTVD  38157  relopabVD  38159  e2ebindVD  38170  stoweidlem35  38928  stoweidlem48  38941  rexrsb  39818  funbrafv  39887  rlimdmafv  39906  fzopredsuc  39946  iccpartlt  39962  proththd  40069  nnsum3primesle9  40210  wtgoldbnnsum4prm  40218  bgoldbnnsum3prm  40220  pfxccatin12lem2  40287  fzoopth  40360  2ffzoeq  40361  usgredgprvALT  40422  fusgrfisstep  40548  fusgrfis  40549  nbupgr  40566  nbumgrvtx  40568  1wlkp1lem8  40889  upgr2pthnlp  40938  isclWlkb  40980  crctisclwlk  41000  cyclnsPth  41006  wwlksnextinj  41105  clwlkclwwlklem2a1  41201  clwwisshclwws  41235  eucrctshift  41411  eucrct2eupth  41413  fusgr2wsp2nb  41498  av-numclwwlkovf2ex  41517  av-numclwwlk2lem1  41532  av-numclwwlk5lem  41541  av-frgrareggt1  41547  av-frgrareg  41548  av-friendship  41553  mgm2mgm  41653  2zrngnmlid  41739  2zrngnmrid  41740  ellcoellss  42018  nneop  42114  fldivexpfllog2  42157  digexp  42199  elpglem2  42254