Theorem imbi1d 331

Description: Deduction adding a consequent to both sides of a logical equivalence. (Contributed by NM, 11-May-1993.) (Proof shortened by Wolf Lammen, 17-Sep-2013.)

Hypothesis

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

Assertion

Ref	Expression
imbi1d	|- ( ph -> ( ( ps -> th ) <-> ( ch -> th ) ) )

Proof of Theorem imbi1d

Step	Hyp	Ref	Expression
1		imbid.1	. . . 4 |- ( ph -> ( ps <-> ch ) )
2	1	biimprd 238	. . 3 |- ( ph -> ( ch -> ps ) )
3	2	imim1d 82	. 2 |- ( ph -> ( ( ps -> th ) -> ( ch -> th ) ) )
4	1	biimpd 219	. . 3 |- ( ph -> ( ps -> ch ) )
5	4	imim1d 82	. 2 |- ( ph -> ( ( ch -> th ) -> ( ps -> th ) ) )
6	3, 5	impbid 202	1 |- ( ph -> ( ( ps -> th ) <-> ( ch -> th ) ) )

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:  imbi12d  334  imbi1  337  imim21b  382  pm5.33  922  con3ALT  1032  con3OLD  1035  19.21t  2073  19.21tOLDOLD  2074  19.21tOLD  2213  axc15  2303  ax12v2OLD  2342  drsb1  2377  ralcom2  3104  raleqf  3134  ralxpxfr2d  3327  alexeqg  3332  mo2icl  3385  sbc19.21g  3502  csbiebg  3556  ralss  3668  r19.37zv  4067  ssuniOLD  4460  intmin4  4506  ssexg  4804  pocl  5042  vtoclr  5164  frsn  5189  fun11  5963  funimass4  6247  dff13  6512  f1mpt  6518  isopolem  6595  oprabid  6677  caovcan  6838  caoftrn  6932  ordunisuc2  7044  tfisi  7058  tfinds  7059  tfindsg  7060  tfindsg2  7061  dfom2  7067  findsg  7093  frxp  7287  dfsmo2  7444  qliftfun  7832  ecoptocl  7837  ecopovtrn  7850  dom2lem  7995  findcard  8199  findcard2  8200  findcard3  8203  fiint  8237  supmo  8358  eqsup  8362  suplub  8366  supisoex  8380  infmo  8401  wemaplem1  8451  wemaplem2  8452  wemapsolem  8455  oemapvali  8581  cantnf  8590  wemapwe  8594  karden  8758  aceq1  8940  zorn2lem1  9318  axrepndlem2  9415  axregndlem2  9425  pwfseqlem4  9484  gruurn  9620  indpi  9729  nqereu  9751  prcdnq  9815  supexpr  9876  ltsosr  9915  supsrlem  9932  supsr  9933  axpre-lttrn  9987  axpre-sup  9990  prodgt0  10868  infm3  10982  prime  11458  raluz  11736  zsupss  11777  uzsupss  11780  xrsupsslem  12137  xrinfmsslem  12138  fz1sbc  12416  ssnn0fi  12784  fi1uzind  13279  brfi1indALT  13282  fi1uzindOLD  13285  brfi1indALTOLD  13288  wrdind  13476  wrd2ind  13477  relexprelg  13778  rtrclreclem3  13800  relexpindlem  13803  relexpind  13804  rtrclind  13805  rexanre  14086  rexico  14093  limsupgle  14208  rlim2lt  14228  rlim3  14229  ello12  14247  ello12r  14248  ello1d  14254  elo12  14258  elo12r  14259  rlimconst  14275  lo1resb  14295  o1resb  14297  rlimcn2  14321  addcn2  14324  mulcn2  14326  reccn2  14327  cn1lem  14328  o1rlimmul  14349  lo1le  14382  caucvgrlem  14403  divrcnv  14584  rpnnen2lem12  14954  sqrt2irr  14979  dfgcd2  15263  exprmfct  15416  isprm5  15419  isprm7  15420  prmdvdsexpr  15429  prmpwdvds  15608  vdwmc2  15683  ramtlecl  15704  ramub  15717  rami  15719  ramcl  15733  firest  16093  mreexexd  16308  mreexexdOLD  16309  acsfn  16320  prslem  16931  ispos  16947  posi  16950  isposd  16955  lubeldm  16981  lubval  16984  glbeldm  16994  glbval  16997  joinval2lem  17008  meetval2lem  17022  pospropd  17134  odlem1  17954  mndodcongi  17962  gexlem1  17994  sylow1lem3  18015  efgredlemb  18159  efgred  18161  frgpnabllem1  18276  isrrg  19288  mplsubglem  19434  mpllsslem  19435  ltbval  19471  opsrval  19474  xrsdsreclb  19793  islindf4  20177  mdetunilem1  20418  mdetunilem3  20420  mdetunilem4  20421  mdetunilem9  20426  chpscmat  20647  chfacffsupp  20661  chfacfscmulfsupp  20664  chfacfpmmulfsupp  20668  istopg  20700  isclo2  20892  neiptoptop  20935  neiptopnei  20936  lmbr  21062  ist0  21124  ist1-2  21151  t1sep2  21173  cmpfi  21211  2ndcdisj  21259  1stccn  21266  iskgen3  21352  ptpjopn  21415  hausdiag  21448  xkopt  21458  ist0-4  21532  isr0  21540  r0sep  21551  fbfinnfr  21645  fmfnfmlem2  21759  fmfnfmlem4  21761  fmfnfm  21762  cnflf  21806  cnfcf  21846  tmdgsum2  21900  tsmsgsum  21942  tsmsres  21947  tsmsf1o  21948  tsmsxplem1  21956  tsmsxp  21958  ustssel  22009  ustincl  22011  ustdiag  22012  ustinvel  22013  ustexhalf  22014  ust0  22023  ustuqtop4  22048  utopsnneiplem  22051  isucn2  22083  iducn  22087  metcnp  22346  metcnpi3  22351  txmetcnp  22352  metucn  22376  ngptgp  22440  nlmvscnlem1  22490  nrginvrcnlem  22495  nghmcn  22549  xrge0tsms  22637  xmetdcn2  22640  metdscn  22659  addcnlem  22667  elcncf1di  22698  ipcnlem1  23044  caucfil  23081  metcld  23104  metcld2  23105  volcn  23374  itg2cnlem2  23529  ellimc2  23641  dveflem  23742  dvne0  23774  mdegleb  23824  mdegle0  23837  ply1divex  23896  fta1g  23927  dgrco  24031  plydivex  24052  fta1  24063  vieta1  24067  abelthlem8  24193  divlogrlim  24381  cxpcn3lem  24488  rlimcnp  24692  cxplim  24698  cxploglim  24704  ftalem1  24799  ftalem2  24800  dvdsmulf1o  24920  ppiublem1  24927  dchrinv  24986  lgseisenlem2  25101  2sqlem6  25148  2sqlem8  25151  2sqlem10  25153  dchrisum0  25209  istrkgc  25353  istrkgb  25354  axtgcgrid  25362  axtg5seg  25364  axtgpasch  25366  axtgeucl  25371  tgcgr4  25426  axlowdimlem15  25836  usgr2wlkneq  26652  usgr2pthlem  26659  friendshipgt3  27256  isnvlem  27465  vacn  27549  nmcvcn  27550  smcnlem  27552  blocni  27660  norm3lemt  28009  isch2  28080  chlimi  28091  omlsii  28262  eigorth  28697  0cnop  28838  0cnfn  28839  idcnop  28840  lnconi  28892  stcltr1i  29133  elat2  29199  funcnv5mpt  29469  xrge0infss  29525  resspos  29659  xrge0tsmsd  29785  qqhcn  30035  qqhucn  30036  esum2d  30155  eulerpartlemgvv  30438  sgn3da  30603  sgnnbi  30607  sgnpbi  30608  tgoldbachgt  30741  axtgupdim2OLD  30746  bnj1145  31061  bnj1171  31068  bnj1172  31069  erdszelem8  31180  mclsval  31460  mclsax  31466  mclsppslem  31480  climuzcnv  31565  elintfv  31662  poseq  31750  frrlem4  31783  nocvxminlem  31893  ifscgr  32151  idinside  32191  brsegle  32215  trer  32310  filnetlem4  32376  dnicn  32482  bj-ssbjust  32618  bj-ssbequ  32629  bj-ssblem1  32630  bj-ssblem2  32631  bj-ssb1a  32632  bj-ssb1  32633  bj-ssbcom3lem  32650  bj-19.21t  32817  wl-sbrimt  33331  fin2so  33396  ptrecube  33409  poimirlem26  33435  poimirlem27  33436  heicant  33444  mbfresfi  33456  itg2addnc  33464  ftc1anc  33493  filbcmb  33535  sdclem2  33538  fdc  33541  fdc1  33542  rngoidmlem  33735  divrngidl  33827  pridlval  33832  smprngopr  33851  inecmo  34120  ax12inda  34233  ax12v2-o  34234  isat3  34594  iscvlat2N  34611  psubspset  35030  ldilfset  35394  ldilset  35395  dilfsetN  35439  dilsetN  35440  cdlemefrs29bpre0  35684  cdlemefrs29clN  35687  cdlemefrs32fva  35688  cdlemn11pre  36499  dihord2pre  36514  lpolsetN  36771  aomclem8  37631  hbtlem5  37698  acsfn1p  37769  ifpbi1  37822  ifpbi12  37833  ifpbi13  37834  ntrneik2  38390  ntrneikb  38392  gneispacess2  38444  2sbc6g  38616  sbiota1  38635  uzwo4  39221  fsumiunss  39807  mullimc  39848  limcdm0  39850  mullimcf  39855  constlimc  39856  idlimc  39858  limsupre  39873  limcleqr  39876  addlimc  39880  0ellimcdiv  39881  limsupref  39917  limsupbnd1f  39918  limsupmnf  39953  limsupre2  39957  limsupmnfuzlem  39958  limsupre2mpt  39962  limsupre3  39965  limsupre3mpt  39966  limsupre3uzlem  39967  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  dvmptfprodlem  40159  wallispilem3  40284  fourierdlem48  40371  fourierdlem87  40410  sge0f1o  40599  sge0iunmptlemre  40632  sge0iunmpt  40635  vonioo  40896  vonicc  40899  bgoldbachlt  41701  tgoldbachlt  41704  bgoldbachltOLD  41707  tgoldbachltOLD  41710  sprsymrelfolem2  41743  ply1mulgsumlem1  42174  ply1mulgsumlem2  42175  elbigo2  42346  elbigo2r  42347  setrecseq  42432  setrec1lem1  42434  aacllem  42547