Theorem imbi2d 314

Description: Deduction adding an antecedent to both sides of a logical equivalence. (Contributed by NM, 11-May-1993.)

Hypothesis

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

Assertion

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

Proof of Theorem imbi2d

Step	Hyp	Ref	Expression
1		imbid.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	a1d 25	. 2 |- ( ph -> ( th -> ( ps <-> ch ) ) )
3	2	pm5.74d 247	1 |- ( ph -> ( ( th -> ps ) <-> ( th -> ch ) ) )

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

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 185

This theorem is referenced by:  imbi12d  318  imbi2  322  pm5.42  546  orbi2d  699  con3th  956  ax12vOLD  1861  ax12v2  2087  axc14  2115  ax12eq  2273  ax12el  2274  ax12indalem  2277  ax12inda2ALT  2278  ax12inda  2280  ax12v2-o  2281  mo2  2295  2eu6OLD  2381  2gencl  3137  3gencl  3138  vtocl2gf  3166  vtocl3gf  3167  vtocl4g  3175  eqeu  3267  mo2icl  3275  euind  3283  reu7  3291  reuind  3300  sbctt  3387  sbcnestgf  3834  r19.36zv  3918  dedth2h  3981  dedth3h  3982  dedth4h  3983  preq12bg  4195  prel12g  4196  elint  4277  elintrabg  4284  intab  4302  trss  4541  axrep1  4551  axrep2  4552  axrep3  4553  bm1.3ii  4563  reusv3  4645  pocl  4796  swopolem  4798  solin  4812  freq1  4838  frminex  4848  vtoclr  5033  2optocl  5066  3optocl  5067  raliunxp  5131  resieq  5272  iss  5309  cnveqb  5446  funmo  5586  funimaexg  5647  fnbrfvb  5888  fvelimab  5904  fvmptss  5940  fmptco  6040  fprg  6056  fnressn  6059  fressnfv  6061  isoselem  6212  ovg  6414  caovcan  6452  caovordig  6453  caovord  6459  tfisi  6666  tfindsg  6668  tfinds2  6671  tfinds3  6672  dfom2  6675  elom  6676  findsg  6700  finds2  6701  f1o2ndf1  6881  poxp  6885  fnse  6890  smoeq  7013  smores  7015  smogt  7030  tfrlem1  7037  tfr3  7060  oaordi  7187  oeordi  7228  oeoa  7238  oeoe  7240  nnacl  7252  nnmcl  7253  nnecl  7254  nnacom  7258  nnaordi  7259  nnawordi  7262  nnaass  7263  nndi  7264  nnmass  7265  nnmsucr  7266  nnmcom  7267  nnmordi  7272  2ecoptocl  7394  3ecoptocl  7395  undifixp  7498  xpdom2g  7606  findcard2  7752  xpfi  7783  fnfi  7790  fodomfi  7791  finsschain  7819  marypha1lem  7885  marypha1  7886  supeq1  7896  ordiso2  7932  ordtypelem7  7941  wemaplem1  7963  inf3lem2  8037  inf3lem5  8040  infdiffi  8065  cantnfval2  8079  cantnfle  8081  cantnfp1lem3  8090  oemapval  8093  cantnflem1  8099  cantnf  8103  cantnfval2OLD  8109  cantnfleOLD  8111  cantnfp1lem3OLD  8116  cantnflem1OLD  8122  cantnfOLD  8125  wemapwe  8130  wemapweOLD  8131  cnfcom  8135  cnfcom3clem  8140  cnfcomOLD  8143  cnfcom3clemOLD  8148  tz9.1  8151  r1pwALT  8255  cplem2  8299  karden  8304  infxpenc2lem2  8388  infxpenc2lem2OLD  8392  fseqenlem1  8396  dfac8clem  8404  alephinit  8467  dfac4  8494  dfac5lem5  8499  dfac2a  8501  dfac2  8502  dfacacn  8512  dfac12lem3  8516  kmlem2  8522  kmlem13  8533  ackbij1lem16  8606  sornom  8648  infpssrlem4  8677  fin23lem14  8704  fin23lem32  8715  fin23lem34  8717  fin23lem36  8719  isf32lem1  8724  isf32lem2  8725  axcc2lem  8807  axcc3  8809  axcclem  8828  zornn0g  8876  ttukeylem5  8884  ttukeylem6  8885  axrepnd  8960  axpowndlem3  8965  zfcndrep  8981  fpwwe2lem8  9004  pwfseqlem3  9027  wunr1om  9086  wunfi  9088  tskr1om  9134  ingru  9182  grudomon  9184  axgroth3  9198  axgroth4  9199  nqereu  9296  mulcanenq  9327  elnp  9354  elnpi  9355  prlem934  9400  infm3  10497  nnaddcl  10553  nnmulcl  10554  peano5uzi  10947  uzind2  10951  uzindOLD  10953  nn0indd  10957  zindd  10961  eluzadd  11110  uzaddcl  11138  uzwo  11145  uzwoOLD  11146  indstr  11151  zmax  11180  xmulasslem  11480  xrsupsslem  11501  xrinfmsslem  11502  xrsupss  11503  xrinfmss  11504  flval2  11931  om2uzlti  12043  uzrdgfni  12051  rabssnn0fi  12077  mptnn0fsupp  12085  seqcl2  12107  seqfveq2  12111  seqshft2  12115  monoord  12119  seqsplit  12122  seqcaopr3  12124  seqf1olem2a  12127  seqf1o  12130  seqid2  12135  seqhomo  12136  ser1const  12145  expcllem  12159  expeq0  12178  mulexp  12187  expadd  12190  expmul  12193  leexp2r  12205  leexp1a  12206  bernneq  12274  modexp  12283  facdiv  12347  faclbnd  12350  faclbnd4lem4  12356  faclbnd6  12359  hashgadd  12428  hashxp  12476  hashmap  12477  hashf1lem2  12489  hashf1  12490  seqcoll  12496  wrdind  12693  wrd2ind  12694  swrdccatin12lem3  12706  cshweqrep  12780  2cshwcshw  12784  relexp0g  12939  relexpsucnnr  12942  relexpsucnnl  12947  relexpcnv  12950  relexpnndm  12956  relexpaddnn  12966  dfrtrclrec2  12972  rtrclreclem1  12973  rtrclreclem2  12974  rtrclreclem4  12976  dfrtrcl2  12977  relexpind  12979  cjexp  13065  absexp  13219  rlim  13400  rlim2  13401  rlim0  13413  rlim0lt  13414  rlimi  13418  ello12r  13422  ello1mpt  13426  ello1d  13428  elo12r  13433  lo1o1  13437  o1lo1  13442  lo1res  13464  climshft  13481  o1compt  13492  rlimo1  13521  lo1add  13531  lo1mul  13532  rlimdiv  13550  climub  13566  climserle  13567  caucvgrlem  13577  caurcvgr  13578  iseraltlem2  13587  summolem2a  13619  sumss  13628  fsum2d  13668  fsumabs  13697  fsumrlim  13707  fsumo1  13708  fsumiun  13717  binom  13724  bcxmas  13729  climcndslem1  13743  climcndslem2  13744  cvgrat  13774  clim2prod  13779  prodfn0  13785  prodfrec  13786  ntrivcvgfvn0  13790  prodmolem2a  13823  fprodabs  13860  fprodn0  13865  fprod2d  13867  fprodefsum  13912  demoivreALT  14018  ruclem8  14054  ruclem9  14055  dvdsle  14115  dvdsfac  14125  divalglem7  14141  bitsinv1  14176  sadcadd  14192  sadadd2  14194  saddisjlem  14198  smuval2  14216  smupvallem  14217  smu01lem  14219  smupval  14222  smueqlem  14224  smumullem  14226  bezoutlem4  14263  gcdmultiple  14272  rplpwr  14278  nn0seqcvgd  14283  seq1st  14284  alginv  14288  algcvga  14292  algfx  14293  prmind2  14312  prmdvdsexp  14339  prmfac1  14343  reumodprminv  14413  pcmpt  14495  pcfac  14502  prmpwdvds  14506  prmreclem4  14521  vdwlem10  14592  ramval  14610  ramcl  14631  cshwrepswhash1  14671  prmlem1a  14676  imasleval  15030  ismre  15079  mreexexd  15137  lubprop  15815  lublecllem  15817  glbprop  15828  joinlem  15840  meetlem  15854  isglbd  15946  lubun  15952  poslubmo  15975  posglbmo  15976  poslubd  15977  mrcmndind  16196  frmdgsum  16229  mulgnnass  16369  mhmmulg  16373  gsumwrev  16600  gsmsymgrfix  16652  gsmsymgreq  16656  psgnunilem3  16720  sylow1lem1  16817  efginvrel2  16944  efgsrel  16951  efgredlemd  16961  efgredlem  16964  efgred  16965  efgrelexlemb  16967  gsum2dlem2  17194  gsum2dOLD  17196  gsumcom2  17199  ablfac1eulem  17318  pgpfac1lem2  17321  pgpfac1lem5  17325  pgpfac1  17326  pgpfac  17330  srgmulgass  17377  srgpcomp  17378  srgbinom  17391  lmodvsmmulgdi  17742  isdomn2  18143  assamulgscm  18194  mplcoe1  18322  mplcoe3  18323  mplcoe3OLD  18324  mplcoe5  18326  mplcoe2OLD  18328  gsummoncoe1  18541  cnfldexp  18646  islindf4  19040  dmatval  19161  dmatel  19162  dmatmulcl  19169  pmatcoe1fsupp  19369  decpmataa0  19436  decpmatmulsumfsupp  19441  pmatcollpw2lem  19445  pm2mpmhmlem1  19486  fiinopn  19577  mretopd  19760  neiptoptop  19799  cnpfval  19902  iscnp3  19912  tgcn  19920  lmbr  19926  lmbr2  19927  lmbrf  19928  lmss  19966  ishaus  19990  hausnei2  20021  t1sep2  20037  fiuncmp  20071  dfcon2  20086  1stcfb  20112  2ndc1stc  20118  1stcrest  20120  1stcelcls  20128  1stccn  20130  lly1stc  20163  elkgen  20203  kgencn  20223  tx1stc  20317  xkopt  20322  cnmptcom  20345  isr0  20404  r0sep  20415  ptcmpfi  20480  isfildlem  20524  rnelfm  20620  fbflim  20643  flimrest  20650  isflf  20660  flffbas  20662  lmflf  20672  fclsrest  20691  isfcf  20701  cnextfvval  20731  tmdmulg  20757  tmdgsum  20760  eltsms  20797  tsmsi  20798  tsmsgsum  20803  tsmsgsumOLD  20806  tsmssubm  20810  tsmsresOLD  20811  tsmsres  20812  tsmsf1o  20813  isust  20872  isucn  20947  isucn2  20948  ucnima  20950  imasdsf1olem  21042  metss  21177  met1stc  21190  metcnp  21210  metcnpi  21213  metcnpi2  21214  metucnOLD  21257  metucn  21258  xrge0tsms  21505  fsumcn  21540  elcncf  21559  cncfi  21564  rescncf  21567  cncfco  21577  caucfil  21888  equivcau  21905  caubl  21912  caublcls  21913  ovolgelb  22057  ovolunlem1a  22073  ovolicc2lem3  22096  voliunlem1  22126  voliunlem3  22128  volsuplem  22131  volsup  22132  dyadmax  22173  vitali  22188  itg2leub  22307  itgfsum  22399  dvnadd  22498  dvnres  22500  cpnord  22504  dvnfre  22521  dvmptfsum  22542  dvferm1  22552  dvferm2  22554  rolle  22557  dvlip  22560  c1lip1  22564  lhop1  22581  deg1leb  22661  ply1divex  22703  fta1g  22734  plyco  22804  dgrcolem1  22836  dgrco  22838  dvnply2  22849  plydivex  22859  aalioulem2  22895  aalioulem3  22896  aalioulem5  22898  aaliou3lem2  22905  dvntaylp  22932  taylthlem1  22934  ulmdvlem3  22963  abelthlem9  23001  cxpmul2  23238  scvxcvx  23513  jensenlem2  23515  jensen  23516  wilthlem3  23542  perfectlem2  23703  bcmono  23750  bposlem5  23761  lgsquad2lem2  23832  dchrisumlem1  23872  dchrisum0flb  23893  pntpbnd1  23969  pntlemf  23988  qabvle  24008  qabvexp  24009  ostthlem2  24011  ostth2lem2  24017  sizeusglecusglem1  24686  2pthoncl  24807  fargshiftf1  24839  3v3e3cycl1  24846  4cycl4v4e  24868  4cycl4dv4e  24870  wlkiswwlk2lem4  24896  wlkiswwlk2  24899  clwlkisclwwlklem2a  24987  clwlkisclwwlklem2  24988  clwlkfoclwwlk  25047  el2wlkonot  25071  el2spthonot  25072  rusgranumwlk  25159  eupatrl  25170  eupath2  25182  frgra3vlem1  25202  3vfriswmgralem  25206  usg2spot2nb  25267  2spotmdisj  25270  numclwlk2lem2f1o  25307  isplig  25381  gxnn0add  25474  gxnn0mul  25477  ghgrpOLD  25568  ghabloOLD  25569  isnvlem  25701  nvi  25705  nmoubi  25885  nmounbi  25889  nmblolbi  25913  ipasslem1  25944  ipassi  25954  hlim2  26307  pjhth  26509  spansni  26673  elspansn2  26683  pjige0  26807  pjcjt2  26808  pjopyth  26836  elcnop  26974  elcnfn  26999  nmopub  27025  cnopc  27030  nmfnleub  27042  elnlfn  27045  cnfnc  27047  nmbdoplb  27142  nmcexi  27143  nmcoplb  27147  lnfnmul  27165  nmbdfnlb  27167  nmcfnlb  27171  pjss2coi  27281  pjssmi  27282  isst  27330  ishst  27331  stcltr1i  27391  mdbr  27411  dmdbr  27416  mddmd2  27426  mdslmd1lem3  27444  mdslmd1lem4  27445  elat2  27457  atcvat2  27506  cdj1i  27550  rmoeq  27584  iuninc  27638  fmptcof2  27724  nn0min  27845  isomnd  27925  omndadd  27930  isarchi2  27963  archirng  27966  archiexdiv  27968  archiabl  27976  xrge0tsmsd  28010  isorng  28024  ofldchr  28039  crefeq  28083  nexple  28239  esumfzf  28298  issiga  28341  isrnsiga  28343  isldsys  28385  ismeas  28407  isrnmeas  28408  measiun  28426  eulerpartlemn  28584  sseqp1  28598  rrvsum  28657  signsply0  28772  signstfvc  28795  subfacp1lem6  28893  erdszelem8  28906  isscon  28935  cvmliftlem7  29000  cvmliftlem10  29003  cvmlift3lem2  29029  mrsubvrs  29146  mclsssvlem  29186  mclsval  29187  mclsax  29193  mclsind  29194  ghomf1olem  29298  shftvalg  29356  iprodefisumlem  29364  binomfallfac  29404  faclimlem1  29409  dfpo2  29425  rdgprc  29467  preddowncl  29516  trpredmintr  29554  frmin  29562  soseq  29574  wfr3g  29582  wfrlem4  29586  frr3g  29626  bpolycl  30042  bpolydif  30045  fveleq  30144  wl-sblimt  30239  wl-sbhbt  30242  wl-2sb6d  30248  wl-mo2dnae  30259  wl-mo2t  30260  heicant  30289  mbfresfi  30301  itg2gt0cn  30310  sdclem2  30475  fdc  30478  seqpo  30480  incsequz  30481  mettrifi  30490  prdsbnd2  30531  heiborlem4  30550  bfplem1  30558  iscringd  30636  maxidlval  30676  igenval2  30703  ismrc  30873  incssnn0  30883  mzpexpmpt  30917  pell14qrexpclnn0  31041  monotuz  31116  expmordi  31122  rmxypos  31124  jm2.17a  31137  jm2.17b  31138  rmygeid  31141  divalgmodcl  31168  jm2.18  31169  jm2.19lem3  31172  jm2.25  31180  jm2.15nn0  31184  jm2.16nn0  31185  wepwsolem  31226  aomclem8  31246  dfac11  31247  pwslnm  31279  lnr2i  31306  hbtlem5  31318  cnsrexpcl  31355  rngunsnply  31363  isdomn3  31405  dvgrat  31434  pm14.122b  31571  fnchoice  31644  fperiodmullem  31742  fmul01  31813  fmuldfeq  31816  climsuselem1  31852  climinff  31856  ellimcabssub0  31862  limcleqr  31889  addlimc  31893  0ellimcdiv  31894  limclner  31896  dvnmptdivc  31974  dvnmptconst  31977  dvnmul  31979  iblspltprt  32011  itgspltprt  32017  stoweidlem2  32023  stoweidlem3  32024  stoweidlem17  32038  stoweidlem19  32040  stoweidlem21  32042  stoweidlem26  32047  fourierdlem42  32170  2ffzoeq  32715  usgra2pth  32726  usgfis  32818  lmodvsmdi  33229  dmatALTval  33255  dmatALTbasel  33257  snlindsntor  33326  ldepsnlinc  33363  elbigo2r  33428  elbigolo1  33432  bnj941  34232  bnj106  34327  bnj155  34338  bnj590  34369  bnj591  34370  bnj849  34384  bnj893  34387  bnj944  34397  bnj1128  34447  bj-con3thALT  34563  bj-axc15v  34731  bj-axrep1  34775  bj-axrep2  34776  bj-axrep3  34777  riotasvd  35084  isopos  35302  isat3  35429  ishlat1  35474  glbconN  35498  ispsubsp  35866  isldil  36231  isltrn  36240  isdilN  36276  trlval  36284  cdleme27b  36491  cdleme29b  36498  cdleme31sn1  36504  cdleme31sn1c  36511  cdleme40v  36592  cdlemk36  37036  cdlemkid5  37058  cdlemn11pre  37334  dihord2pre  37349  islpolN  37607  hdmapffval  37953  hdmapfval  37954  hdmapval2lem  37958  ifpbi23  38101  eliunov2  38200  iunrelexpmin1  38207  iunrelexpmin2  38208  relexpss1d  38217  relexpiidm  38222  relexp0a  38223  relexpxpnnidm  38225  relexpmulnn  38227