Theorem imbi2d 316

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  320  imbi2  324  pm5.42  548  orbi2d  701  con3th  956  ax12vOLD  1840  ax12v2  2067  axc14  2097  ax12eq  2255  ax12el  2256  ax12indalem  2259  ax12inda2ALT  2260  ax12inda  2262  ax12v2-o  2263  mo2  2277  2eu6OLD  2368  2gencl  3124  3gencl  3125  vtocl2gf  3153  vtocl3gf  3154  vtocl4g  3162  eqeu  3254  mo2icl  3262  euind  3270  reu7  3278  reuind  3287  sbctt  3382  sbcnestgf  3822  r19.36zv  3912  dedth2h  3976  dedth3h  3977  dedth4h  3978  preq12bg  4191  prel12g  4192  elint  4274  elintrabg  4281  intab  4299  trss  4536  axrep1  4546  axrep2  4547  axrep3  4548  bm1.3ii  4558  reusv3  4642  pocl  4794  swopolem  4796  solin  4810  freq1  4836  frminex  4846  vtoclr  5031  2optocl  5064  3optocl  5065  raliunxp  5129  resieq  5271  iss  5308  cnveqb  5449  funmo  5591  funimaexg  5652  fnbrfvb  5895  fvelimab  5911  fvmptss  5946  fmptco  6046  fprg  6062  fnressn  6065  fressnfv  6067  isoselem  6219  ovg  6423  caovcan  6461  caovordig  6462  caovord  6468  tfisi  6675  tfindsg  6677  tfinds2  6680  tfinds3  6681  dfom2  6684  elom  6685  findsg  6709  finds2  6710  f1o2ndf1  6890  poxp  6894  fnse  6899  smoeq  7020  smores  7022  smogt  7037  tfrlem1  7044  tfr3  7067  oaordi  7194  oeordi  7235  oeoa  7245  oeoe  7247  nnacl  7259  nnmcl  7260  nnecl  7261  nnacom  7265  nnaordi  7266  nnawordi  7269  nnaass  7270  nndi  7271  nnmass  7272  nnmsucr  7273  nnmcom  7274  nnmordi  7279  2ecoptocl  7401  3ecoptocl  7402  undifixp  7504  xpdom2g  7612  findcard2  7759  xpfi  7790  fnfi  7797  fodomfi  7798  finsschain  7826  marypha1lem  7892  marypha1  7893  supeq1  7904  ordiso2  7940  ordtypelem7  7949  wemaplem1  7971  inf3lem2  8046  inf3lem5  8049  infdiffi  8074  cantnfval2  8088  cantnfle  8090  cantnfp1lem3  8099  oemapval  8102  cantnflem1  8108  cantnf  8112  cantnfval2OLD  8118  cantnfleOLD  8120  cantnfp1lem3OLD  8125  cantnflem1OLD  8131  cantnfOLD  8134  wemapwe  8139  wemapweOLD  8140  cnfcom  8144  cnfcom3clem  8149  cnfcomOLD  8152  cnfcom3clemOLD  8157  tz9.1  8160  r1pwOLD  8264  cplem2  8308  karden  8313  infxpenc2lem2  8397  infxpenc2lem2OLD  8401  fseqenlem1  8405  dfac8clem  8413  alephinit  8476  dfac4  8503  dfac5lem5  8508  dfac2a  8510  dfac2  8511  dfacacn  8521  dfac12lem3  8525  kmlem2  8531  kmlem13  8542  ackbij1lem16  8615  sornom  8657  infpssrlem4  8686  fin23lem14  8713  fin23lem32  8724  fin23lem34  8726  fin23lem36  8728  isf32lem1  8733  isf32lem2  8734  axcc2lem  8816  axcc3  8818  axcclem  8837  zornn0g  8885  ttukeylem5  8893  ttukeylem6  8894  axrepnd  8969  axpowndlem3  8975  axpowndlem3OLD  8976  zfcndrep  8992  fpwwe2lem8  9015  pwfseqlem3  9038  wunr1om  9097  wunfi  9099  tskr1om  9145  ingru  9193  grudomon  9195  axgroth3  9209  axgroth4  9210  nqereu  9307  mulcanenq  9338  elnp  9365  elnpi  9366  prlem934  9411  infm3  10505  nnaddcl  10561  nnmulcl  10562  peano5uzi  10954  uzind2  10958  uzindOLD  10960  zindd  10967  eluzadd  11115  uzaddcl  11143  uzwo  11150  uzwoOLD  11151  indstr  11156  zmax  11185  xmulasslem  11483  xrsupsslem  11504  xrinfmsslem  11505  xrsupss  11506  xrinfmss  11507  flval2  11926  om2uzlti  12037  uzrdgfni  12045  rabssnn0fi  12071  mptnn0fsupp  12079  seqcl2  12101  seqfveq2  12105  seqshft2  12109  monoord  12113  seqsplit  12116  seqcaopr3  12118  seqf1olem2a  12121  seqf1o  12124  seqid2  12129  seqhomo  12130  ser1const  12139  expcllem  12153  expeq0  12172  mulexp  12181  expadd  12184  expmul  12187  leexp2r  12199  leexp1a  12200  bernneq  12268  modexp  12277  facdiv  12341  faclbnd  12344  faclbnd4lem4  12350  faclbnd6  12353  hashgadd  12421  hashxp  12468  hashmap  12469  hashf1lem2  12481  hashf1  12482  seqcoll  12488  wrdind  12678  wrd2ind  12679  swrdccatin12lem3  12691  cshweqrep  12765  2cshwcshw  12769  cjexp  12959  absexp  13113  rlim  13294  rlim2  13295  rlim0  13307  rlim0lt  13308  rlimi  13312  ello12r  13316  ello1mpt  13320  ello1d  13322  elo12r  13327  lo1o1  13331  o1lo1  13336  lo1res  13358  climshft  13375  o1compt  13386  rlimo1  13415  lo1add  13425  lo1mul  13426  rlimdiv  13444  climub  13460  climserle  13461  caucvgrlem  13471  caurcvgr  13472  iseraltlem2  13481  summolem2a  13513  sumss  13522  fsum2d  13562  fsumabs  13591  fsumrlim  13601  fsumo1  13602  fsumiun  13611  binom  13618  bcxmas  13623  climcndslem1  13637  climcndslem2  13638  cvgrat  13668  demoivreALT  13810  ruclem8  13844  ruclem9  13845  dvdsle  13905  dvdsfac  13915  divalglem7  13931  bitsinv1  13966  sadcadd  13982  sadadd2  13984  saddisjlem  13988  smuval2  14006  smupvallem  14007  smu01lem  14009  smupval  14012  smueqlem  14014  smumullem  14016  bezoutlem4  14053  gcdmultiple  14062  rplpwr  14068  nn0seqcvgd  14073  seq1st  14074  alginv  14078  algcvga  14082  algfx  14083  prmind2  14102  prmdvdsexp  14129  prmfac1  14133  reumodprminv  14203  pcmpt  14285  pcfac  14292  prmpwdvds  14296  prmreclem4  14311  vdwlem10  14382  ramval  14400  ramcl  14421  cshwrepswhash1  14461  prmlem1a  14466  imasleval  14812  ismre  14861  mreexexd  14919  lubprop  15487  lublecllem  15489  glbprop  15500  joinlem  15512  meetlem  15526  isglbd  15618  lubun  15624  poslubmo  15647  posglbmo  15648  poslubd  15649  mrcmndind  15868  frmdgsum  15901  mulgnnass  16041  mhmmulg  16045  gsumwrev  16272  gsmsymgrfix  16324  gsmsymgreq  16328  psgnunilem3  16392  sylow1lem1  16489  efginvrel2  16616  efgsrel  16623  efgredlemd  16633  efgredlem  16636  efgred  16637  efgrelexlemb  16639  gsum2dlem2  16869  gsum2dOLD  16871  gsumcom2  16874  ablfac1eulem  16994  pgpfac1lem2  16997  pgpfac1lem5  17001  pgpfac1  17002  pgpfac  17006  srgmulgass  17053  srgpcomp  17054  srgbinom  17067  lmodvsmmulgdi  17418  isdomn2  17819  assamulgscm  17870  mplcoe1  17998  mplcoe3  17999  mplcoe3OLD  18000  mplcoe5  18002  mplcoe2OLD  18004  gsummoncoe1  18217  cnfldexp  18322  islindf4  18743  dmatval  18864  dmatel  18865  dmatmulcl  18872  pmatcoe1fsupp  19072  decpmataa0  19139  decpmatmulsumfsupp  19144  pmatcollpw2lem  19148  pm2mpmhmlem1  19189  fiinopn  19280  mretopd  19463  neiptoptop  19502  cnpfval  19605  iscnp3  19615  tgcn  19623  lmbr  19629  lmbr2  19630  lmbrf  19631  lmss  19669  ishaus  19693  hausnei2  19724  t1sep2  19740  fiuncmp  19774  dfcon2  19790  1stcfb  19816  2ndc1stc  19822  1stcrest  19824  1stcelcls  19832  1stccn  19834  lly1stc  19867  elkgen  19907  kgencn  19927  tx1stc  20021  xkopt  20026  cnmptcom  20049  isr0  20108  r0sep  20119  ptcmpfi  20184  isfildlem  20228  rnelfm  20324  fbflim  20347  flimrest  20354  isflf  20364  flffbas  20366  lmflf  20376  fclsrest  20395  isfcf  20405  cnextfvval  20435  tmdmulg  20461  tmdgsum  20464  eltsms  20501  tsmsi  20502  tsmsgsum  20507  tsmsgsumOLD  20510  tsmssubm  20514  tsmsresOLD  20515  tsmsres  20516  tsmsf1o  20517  isust  20576  isucn  20651  isucn2  20652  ucnima  20654  imasdsf1olem  20746  metss  20881  met1stc  20894  metcnp  20914  metcnpi  20917  metcnpi2  20918  metucnOLD  20961  metucn  20962  xrge0tsms  21209  fsumcn  21244  elcncf  21263  cncfi  21268  rescncf  21271  cncfco  21281  caucfil  21592  equivcau  21609  caubl  21616  caublcls  21617  ovolgelb  21761  ovolunlem1a  21777  ovolicc2lem3  21800  voliunlem1  21830  voliunlem3  21832  volsuplem  21835  volsup  21836  dyadmax  21877  vitali  21892  itg2leub  22011  itgfsum  22103  dvnadd  22202  dvnres  22204  cpnord  22208  dvnfre  22225  dvmptfsum  22246  dvferm1  22256  dvferm2  22258  rolle  22261  dvlip  22264  c1lip1  22268  lhop1  22285  deg1leb  22365  ply1divex  22407  fta1g  22438  plyco  22508  dgrcolem1  22539  dgrco  22541  dvnply2  22552  plydivex  22562  aalioulem2  22598  aalioulem3  22599  aalioulem5  22601  aaliou3lem2  22608  dvntaylp  22635  taylthlem1  22637  ulmdvlem3  22666  abelthlem9  22704  cxpmul2  22939  scvxcvx  23184  jensenlem2  23186  jensen  23187  wilthlem3  23213  perfectlem2  23374  bcmono  23421  bposlem5  23432  lgsquad2lem2  23503  dchrisumlem1  23543  dchrisum0flb  23564  pntpbnd1  23640  pntlemf  23659  qabvle  23679  qabvexp  23680  ostthlem2  23682  ostth2lem2  23688  sizeusglecusglem1  24353  2pthoncl  24474  fargshiftf1  24506  3v3e3cycl1  24513  4cycl4v4e  24535  4cycl4dv4e  24537  wlkiswwlk2lem4  24563  wlkiswwlk2  24566  clwlkisclwwlklem2a  24654  clwlkisclwwlklem2  24655  clwlkfoclwwlk  24714  el2wlkonot  24738  el2spthonot  24739  rusgranumwlk  24826  eupatrl  24837  eupath2  24849  frgra3vlem1  24869  3vfriswmgralem  24873  usg2spot2nb  24934  2spotmdisj  24937  numclwlk2lem2f1o  24974  isplig  25048  gxnn0add  25145  gxnn0mul  25148  ghgrpOLD  25239  ghabloOLD  25240  isnvlem  25372  nvi  25376  nmoubi  25556  nmounbi  25560  nmblolbi  25584  ipasslem1  25615  ipassi  25625  hlim2  25978  pjhth  26180  spansni  26344  elspansn2  26354  pjige0  26478  pjcjt2  26479  pjopyth  26507  elcnop  26645  elcnfn  26670  nmopub  26696  cnopc  26701  nmfnleub  26713  elnlfn  26716  cnfnc  26718  nmbdoplb  26813  nmcexi  26814  nmcoplb  26818  lnfnmul  26836  nmbdfnlb  26838  nmcfnlb  26842  pjss2coi  26952  pjssmi  26953  isst  27001  ishst  27002  stcltr1i  27062  mdbr  27082  dmdbr  27087  mddmd2  27097  mdslmd1lem3  27115  mdslmd1lem4  27116  elat2  27128  atcvat2  27177  cdj1i  27221  rmoeq  27255  iuninc  27297  fmptcof2  27371  nn0indd  27479  nn0min  27481  isomnd  27561  omndadd  27566  isarchi2  27599  archirng  27602  archiexdiv  27604  archiabl  27612  xrge0tsmsd  27645  isorng  27659  ofldchr  27674  crefeq  27718  nexple  27875  esumfzf  27945  issiga  27981  isrnsiga  27983  ismeas  28040  isrnmeas  28041  measiun  28059  eulerpartlemn  28190  sseqp1  28204  rrvsum  28263  signsply0  28378  signstfvc  28401  subfacp1lem6  28499  erdszelem8  28512  isscon  28541  cvmliftlem7  28606  cvmliftlem10  28609  cvmlift3lem2  28635  mrsubvrs  28752  mclsssvlem  28792  mclsval  28793  mclsax  28799  mclsind  28800  ghomf1olem  28904  relexp0  28922  relexpsucr  28923  relexpsucl  28925  relexpind  28933  dfrtrclrec2  28936  rtrclreclem.refl  28937  rtrclreclem.subset  28938  rtrclreclem.min  28940  dfrtrcl2  28941  shftvalg  28986  clim2prod  28994  prodfn0  29000  prodfrec  29001  ntrivcvgfvn0  29005  prodmolem2a  29038  fprodabs  29075  fprodefsum  29076  fprodn0  29081  fprod2d  29083  iprodefisumlem  29095  binomfallfac  29135  faclimlem1  29140  dfpo2  29156  rdgprc  29199  preddowncl  29248  trpredmintr  29286  frmin  29294  soseq  29306  wfr3g  29314  wfrlem4  29318  frr3g  29358  bpolycl  29786  bpolydif  29789  fveleq  29888  wl-sblimt  29971  wl-sbhbt  29974  wl-2sb6d  29980  wl-mo2dnae  29991  wl-mo2t  29992  heicant  30021  mbfresfi  30033  itg2gt0cn  30042  sdclem2  30207  fdc  30210  seqpo  30212  incsequz  30213  mettrifi  30222  prdsbnd2  30263  heiborlem4  30282  bfplem1  30290  iscringd  30368  maxidlval  30408  igenval2  30435  ismrc  30605  incssnn0  30615  mzpexpmpt  30649  pell14qrexpclnn0  30774  monotuz  30849  expmordi  30855  rmxypos  30857  jm2.17a  30870  jm2.17b  30871  rmygeid  30874  divalgmodcl  30901  jm2.18  30902  jm2.19lem3  30905  jm2.25  30913  jm2.15nn0  30917  jm2.16nn0  30918  wepwsolem  30959  aomclem8  30979  dfac11  30980  pwslnm  31012  lnr2i  31037  hbtlem5  31049  cnsrexpcl  31087  rngunsnply  31095  isdomn3  31137  dvgrat  31166  pm14.122b  31281  fnchoice  31355  fperiodmullem  31452  fmul01  31502  fmuldfeq  31505  climsuselem1  31521  climinff  31525  ellimcabssub0  31531  limcleqr  31558  addlimc  31562  0ellimcdiv  31563  limclner  31565  iblspltprt  31662  itgspltprt  31668  stoweidlem2  31673  stoweidlem3  31674  stoweidlem17  31688  stoweidlem19  31690  stoweidlem21  31692  stoweidlem26  31697  fourierdlem42  31820  2ffzoeq  32179  usgra2pth  32192  usgfis  32284  lmodvsmdi  32705  dmatALTval  32731  dmatALTbasel  32733  snlindsntor  32802  ldepsnlinc  32839  bnj941  33559  bnj106  33654  bnj155  33665  bnj590  33696  bnj591  33697  bnj849  33711  bnj893  33714  bnj944  33724  bnj1128  33774  bj-con3ALT  33896  bj-axc15v  34063  bj-axrep1  34107  bj-axrep2  34108  bj-axrep3  34109  riotasvd  34410  isopos  34628  isat3  34755  ishlat1  34800  glbconN  34824  ispsubsp  35192  isldil  35557  isltrn  35566  isdilN  35602  trlval  35610  cdleme27b  35817  cdleme29b  35824  cdleme31sn1  35830  cdleme31sn1c  35837  cdleme40v  35918  cdlemk36  36362  cdlemkid5  36384  cdlemn11pre  36660  dihord2pre  36675  islpolN  36933  hdmapffval  37279  hdmapfval  37280  hdmapval2lem  37284