Theorem biimprd 238

Description: Deduce a converse implication from a logical equivalence. Deduction associated with biimpr 210 and biimpri 218. (Contributed by NM, 11-Jan-1993.) (Proof shortened by Wolf Lammen, 22-Sep-2013.)

Hypothesis

Ref	Expression
biimprd.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
biimprd	|- ( ph -> ( ch -> ps ) )

Proof of Theorem biimprd

Step	Hyp	Ref	Expression
1		id 22	. 2 |- ( ch -> ch )
2		biimprd.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	syl5ibr 236	1 |- ( ph -> ( ch -> ps ) )

Syntax hints:   -> wi 4   <-> wb 196

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 197

This theorem is referenced by:  syl6bir  244  mpbird  247  sylibrd  249  sylbird  250  con4bid  307  mtbid  314  mtbii  316  imbi1d  331  biimpar  502  prlem1  1005  alexbii  1760  spfw  1965  spfwOLD  1966  cbvalw  1968  alcomiw  1971  axc11nlemOLD2  1988  ax12vOLDOLD  2051  axc11nlemOLD  2160  cbvalv1  2175  nfimdOLD  2226  cbval  2271  axc11nlemALT  2306  axc16i  2322  axc16gALT  2367  eqrdav  2621  pm13.18  2875  rspcimdv  3310  rspcedv  3313  moi2  3387  moi  3389  eqrdOLD  3623  sspsstr  3712  eqoreldifOLD  4226  rabsnifsb  4257  ralxfrdOLD  4880  ralxfr2d  4882  isso2i  5067  wefrc  5108  elres  5435  sotri3  5526  oneqmini  5776  ordsssuc2  5814  ordtri2or  5822  2elresin  6002  f1ocnv  6149  tz6.12c  6213  fveqres  6230  fvun1  6269  dffo4  6375  funopsn  6413  fconst5  6471  fnprb  6472  fntpb  6473  isores3  6585  f1owe  6603  weniso  6604  ndmovordi  6825  abnexg  6964  orduniorsuc  7030  ordzsl  7045  tfinds  7059  f1oweALT  7152  fnse  7294  tposfo2  7375  wfrlem5  7419  wfrlem12  7426  issmo2  7446  iordsmo  7454  smoel2  7460  tz7.48lem  7536  oawordeulem  7634  om00  7655  omlimcl  7658  odi  7659  nnawordi  7701  fiint  8237  fipreima  8272  dffi2  8329  suplub2  8367  wemapsolem  8455  unwdomg  8489  inf3lem3  8527  trcl  8604  fidomtri  8819  prdom2  8829  cardaleph  8912  ackbij1lem16  9057  coflim  9083  coftr  9095  infpssrlem4  9128  isfin7-2  9218  axdc3lem2  9273  axdc3lem4  9275  brdom6disj  9354  entric  9379  fpwwe2lem12  9463  inatsk  9600  grur1a  9641  indpi  9729  reclem3pr  9871  supsrlem  9932  lelttr  10128  dedekindle  10201  negn0  10459  fimaxre  10968  nnmulcl  11043  arch  11289  nnnegz  11380  zeo  11463  uzm1  11718  rpneg  11863  xrlttri  11972  xrlelttr  11987  iccid  12220  icoshft  12294  fzen  12358  elfz1b  12409  elfz2nn0  12431  elfzom1p1elfzo  12547  fleqceilz  12653  zmodidfzoimp  12700  modsumfzodifsn  12743  hasheqf1oi  13140  hasheqf1oiOLD  13141  hashnfinnn0  13152  hashle2prv  13260  swrd0  13434  swrdccatin12lem2  13489  swrdccat  13493  swrdccat3blem  13495  repswswrd  13531  trclublem  13734  max0add  14050  abslt  14054  absle  14055  rexuzre  14092  caurcvg  14407  caucvg  14409  dvdsval2  14986  negdvdsb  14998  muldvds2  15007  dvdsabseq  15035  smuval2  15204  smupvallem  15205  rplpwr  15276  alginv  15288  algfx  15293  coprmgcdb  15362  divgcdcoprm0  15379  prmgt1  15409  oddprmgt2  15411  rpexp1i  15433  qnumdencl  15447  phiprmpw  15481  prmdiveq  15491  prm23lt5  15519  pcmpt  15596  infpnlem1  15614  prmgaplem3  15757  prmgaplem8  15762  imasaddfnlem  16188  plelttr  16972  lubval  16984  lublecllem  16988  glbval  16997  mrcmndind  17366  mndodconglem  17960  elfrlmbasn0  20106  mavmulsolcl  20357  slesolex  20488  fvmptnn04if  20654  chfacfisf  20659  chfacfisfcpmat  20660  cnpnei  21068  unconn  21232  comppfsc  21335  kqsat  21534  isr0  21540  qtophmeo  21620  trufil  21714  alexsubALT  21855  cnextcn  21871  ucnima  22085  iducn  22087  bl2in  22205  addcnlem  22667  rescncf  22700  ovoliunlem2  23271  voliun  23322  mbflimsup  23433  itgcn  23609  dvdsq1p  23920  aalioulem2  24088  recosf1o  24281  logrec  24501  xrlimcnp  24695  basellem4  24810  bposlem1  25009  bposlem5  25013  lgsqrmod  25077  lgsdchrval  25079  2lgslem1a1  25114  pntlem3  25298  brbtwn2  25785  axbtwnid  25819  umgredgprv  26002  umgrpredgv  26035  usgredgprvALT  26087  fusgrfisstep  26221  fusgrfis  26222  nbupgr  26240  nbumgrvtx  26242  finsumvtxdg2size  26446  wlkp1lem8  26577  upgr2pthnlp  26628  wwlksnextinj  26794  clwlkclwwlklem2a1  26893  clwwisshclwws  26928  eucrctshift  27103  eucrct2eupth  27105  numclwwlkovf2exlem2  27212  numclwwlk2lem1  27235  numclwwlk5lem  27245  frgrreggt1  27251  frgrreg  27252  friendship  27257  blocn2  27663  htthlem  27774  axhcompl-zf  27855  spanuni  28403  spansncol  28427  spansneleq  28429  elspansn5  28433  idcnop  28840  pjnormssi  29027  dmdmd  29159  bian1d  29306  ifeqeqx  29361  supxrnemnf  29534  rexdiv  29634  xrstos  29679  xrge0omnd  29711  cnre2csqlem  29956  fsumcvg4  29996  lmxrge0  29998  qqhval2lem  30025  esumpr2  30129  esumcvg  30148  issgon  30186  measxun2  30273  measres  30285  measdivcstOLD  30287  measdivcst  30288  elorrvc  30525  signsply0  30628  bnj580  30983  erdsze2lem2  31186  cvmsval  31248  fundmpss  31664  dfon2lem3  31690  frmin  31739  poseq  31750  soseq  31751  frrlem5  31784  frrlem11  31792  nosupbnd1  31860  dfrdg4  32058  cgrtriv  32109  btwntriv2  32119  ifscgr  32151  lineext  32183  btwnconn1lem12  32205  colinbtwnle  32225  elicc3  32311  ontgval  32430  onsucconni  32436  bj-bibibi  32571  bj-cbvexw  32664  bj-equsal  32813  bj-restn0  33043  bj-snmoore  33068  bj-elid  33085  bj-finsumval0  33147  relowlssretop  33211  sucneqond  33213  finxpsuc  33235  wl-nfs1t  33324  finixpnum  33394  ltflcei  33397  matunitlindflem1  33405  poimirlem23  33432  poimirlem24  33433  poimirlem27  33436  poimirlem32  33441  itg2addnclem  33461  areacirclem2  33501  areacirclem5  33504  areacirc  33505  nninfnub  33547  prdstotbnd  33593  heiborlem4  33613  heibor  33620  elghomlem2OLD  33685  grpokerinj  33692  isidlc  33814  prtlem17  34161  dral1-o  34189  axc16g-o  34219  lsator0sp  34288  atlrelat1  34608  cvratlem  34707  diaintclN  36347  dibintclN  36456  cdlemn11pre  36499  dihord2pre  36514  dihintcl  36633  dochkrshp4  36678  lcfrlem9  36839  lcfrlem21  36852  mapdh8e  37073  elrfirn2  37259  rencldnfilem  37384  sdrgacs  37771  refimssco  37913  rtrclex  37924  intimasn  37949  ss2iundf  37951  ov2ssiunov2  37992  comptiunov2i  37998  iunrelexpuztr  38011  dssmapf1od  38315  snelpwrVD  39066  en3lplem1VD  39078  en3lpVD  39080  orbi1rVD  39083  sbc3orgVD  39086  3impexpVD  39091  equncomVD  39104  trsbcVD  39113  trintALTVD  39116  trintALT  39117  csbingVD  39120  csbsngVD  39129  csbxpgVD  39130  csbrngVD  39132  csbfv12gALTVD  39135  relopabVD  39137  e2ebindVD  39148  xlimbr  40053  stoweidlem35  40252  stoweidlem48  40265  rexrsb  41169  funbrafv  41238  rlimdmafv  41257  fzopredsuc  41333  fzoopth  41337  2ffzoeq  41338  iccpartlt  41360  pfxccatin12lem2  41424  proththd  41531  even3prm2  41628  sbgoldbm  41672  nnsum3primesle9  41682  wtgoldbnnsum4prm  41690  bgoldbnnsum3prm  41692  mgm2mgm  41863  2zrngnmlid  41949  2zrngnmrid  41950  ellcoellss  42224  nneop  42320  fldivexpfllog2  42359  digexp  42401  elpglem2  42455