Theorem imbi2d 317

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 26	. 2 |- ( ph -> ( th -> ( ps <-> ch ) ) )
3	2	pm5.74d 250	1 |- ( ph -> ( ( th -> ps ) <-> ( th -> ch ) ) )

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

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 188

This theorem is referenced by:  imbi12d  321  imbi2  325  pm5.42  550  orbi2d  706  con3th  966  ax12vOLD  1911  ax12v2  2143  axc14  2171  mo2  2279  2gencl  3048  3gencl  3049  vtocl2gf  3077  vtocl3gf  3078  vtocl4g  3086  eqeu  3177  mo2icl  3185  euind  3193  reu7  3201  reuind  3211  sbctt  3298  sbcnestgf  3750  r19.36zv  3836  dedth2h  3899  dedth3h  3900  dedth4h  3901  preq12bg  4115  prel12g  4116  elint  4197  elintrabg  4204  intab  4222  trss  4463  axrep1  4473  axrep2  4474  axrep3  4475  bm1.3ii  4485  reusv3  4568  pocl  4717  swopolem  4719  solin  4733  freq1  4759  frminex  4769  vtoclr  4834  2optocl  4867  3optocl  4868  raliunxp  4929  resieq  5070  iss  5107  cnveqb  5246  preddowncl  5362  funmo  5553  funimaexg  5614  fnbrfvb  5858  fvelimab  5874  fvmptss  5911  fmptco  6008  fprg  6025  fnressn  6028  fressnfv  6030  isoselem  6184  ovg  6386  caovcan  6424  caovordig  6425  caovord  6431  tfisi  6636  tfindsg  6638  tfinds2  6641  tfinds3  6642  dfom2  6645  elom  6646  findsg  6671  finds2  6672  f1o2ndf1  6852  poxp  6856  fnse  6861  wfr3g  6982  wfrlem4  6987  smoeq  7017  smores  7019  smogt  7034  tfrlem1  7042  tfr3  7065  oaordi  7195  oeordi  7236  oeoa  7246  oeoe  7248  nnacl  7260  nnmcl  7261  nnecl  7262  nnacom  7266  nnaordi  7267  nnawordi  7270  nnaass  7271  nndi  7272  nnmass  7273  nnmsucr  7274  nnmcom  7275  nnmordi  7280  2ecoptocl  7402  3ecoptocl  7403  undifixp  7506  xpdom2g  7614  findcard2  7757  xpfi  7788  fnfi  7795  fodomfi  7796  finsschain  7827  marypha1lem  7893  marypha1  7894  supeq1  7905  ordiso2  7976  ordtypelem7  7985  wemaplem1  8007  inf3lem2  8080  inf3lem5  8083  infdiffi  8108  cantnfval2  8119  cantnfle  8121  cantnfp1lem3  8130  oemapval  8133  cantnflem1  8139  cantnf  8143  wemapwe  8147  cnfcom  8150  cnfcom3clem  8155  tz9.1  8158  r1pwALT  8262  cplem2  8306  karden  8311  infxpenc2lem2  8395  fseqenlem1  8399  dfac8clem  8407  alephinit  8470  dfac4  8497  dfac5lem5  8502  dfac2a  8504  dfac2  8505  dfacacn  8515  dfac12lem3  8519  kmlem2  8525  kmlem13  8536  ackbij1lem16  8609  sornom  8651  infpssrlem4  8680  fin23lem14  8707  fin23lem32  8718  fin23lem34  8720  fin23lem36  8722  isf32lem1  8727  isf32lem2  8728  axcc2lem  8810  axcc3  8812  axcclem  8831  zornn0g  8879  ttukeylem5  8887  ttukeylem6  8888  axrepnd  8963  axpowndlem3  8968  zfcndrep  8983  fpwwe2lem8  9006  pwfseqlem3  9029  wunr1om  9088  wunfi  9090  tskr1om  9136  ingru  9184  grudomon  9186  axgroth3  9200  axgroth4  9201  nqereu  9298  mulcanenq  9329  elnp  9356  elnpi  9357  prlem934  9402  infm3  10512  nnaddcl  10575  nnmulcl  10576  peano5uzi  10968  uzind2  10972  nn0indd  10976  zindd  10980  eluzadd  11131  uzaddcl  11159  uzwo  11166  indstr  11171  zmax  11205  xmulasslem  11515  xrsupsslem  11536  xrinfmsslem  11537  xrsupss  11538  xrinfmss  11539  flval2  11992  om2uzlti  12107  uzrdgfni  12115  rabssnn0fi  12141  mptnn0fsupp  12152  seqcl2  12174  seqfveq2  12178  seqshft2  12182  monoord  12186  seqsplit  12189  seqcaopr3  12191  seqf1olem2a  12194  seqf1o  12197  seqid2  12202  seqhomo  12203  ser1const  12212  expcllem  12226  expeq0  12245  mulexp  12254  expadd  12257  expmul  12260  leexp2r  12273  leexp1a  12274  bernneq  12341  modexp  12350  facdiv  12415  faclbnd  12418  faclbnd4lem4  12424  faclbnd6  12427  hashgadd  12499  hashxp  12547  hashmap  12548  hashf1lem2  12560  hashf1  12561  seqcoll  12568  wrdind  12772  wrd2ind  12773  swrdccatin12lem3  12785  cshweqrep  12859  2cshwcshw  12863  relexp0g  13022  relexpsucnnr  13025  relexpsucnnl  13032  relexpcnv  13035  relexpnndm  13041  relexpaddnn  13051  dfrtrclrec2  13057  rtrclreclem1  13058  rtrclreclem2  13059  rtrclreclem4  13061  dfrtrcl2  13062  relexpind  13064  cjexp  13150  absexp  13304  rlim  13495  rlim2  13496  rlim0  13508  rlim0lt  13509  rlimi  13513  ello12r  13517  ello1mpt  13521  ello1d  13523  elo12r  13528  lo1o1  13532  o1lo1  13537  lo1res  13559  climshft  13576  o1compt  13587  rlimo1  13616  lo1add  13626  lo1mul  13627  rlimdiv  13645  climub  13661  climserle  13662  caucvgrlem  13672  caucvgrlemOLD  13673  caurcvgr  13674  caurcvgrOLD  13675  iseraltlem2  13685  summolem2a  13717  sumss  13726  fsum2d  13768  fsumabs  13797  fsumrlim  13807  fsumo1  13808  fsumiun  13817  binom  13824  bcxmas  13829  climcndslem1  13843  climcndslem2  13844  cvgrat  13875  clim2prod  13880  prodfn0  13886  prodfrec  13887  ntrivcvgfvn0  13891  prodmolem2a  13924  fprodabs  13964  fprodn0  13969  fprod2d  13971  binomfallfac  14030  bpolycl  14041  bpolydif  14044  fprodefsum  14085  demoivreALT  14191  ruclem8  14225  ruclem9  14226  dvdsle  14286  dvdsfac  14296  divalglem7  14315  bitsinv1  14352  sadcadd  14368  sadadd2  14370  saddisjlem  14374  smuval2  14392  smupvallem  14393  smu01lem  14395  smupval  14398  smueqlem  14400  smumullem  14402  bezoutlem4OLD  14442  bezoutlem4  14445  gcdmultiple  14454  rplpwr  14460  nn0seqcvgd  14465  seq1st  14466  alginv  14470  algcvga  14474  algfx  14475  lcmf  14542  prmind2  14571  prmdvdsexp  14603  prmfac1  14607  reumodprminv  14691  pcmpt  14773  pcfac  14780  prmpwdvds  14784  prmreclem4  14799  vdwlem10  14876  ramval  14896  ramvalOLD  14897  ramcl  14923  cshwrepswhash1  15009  prmlem1a  15014  imasleval  15383  ismre  15432  mreexexd  15490  lubprop  16168  lublecllem  16170  glbprop  16181  joinlem  16193  meetlem  16207  isglbd  16299  lubun  16305  poslubmo  16328  posglbmo  16329  poslubd  16330  mrcmndind  16549  frmdgsum  16582  mulgnnass  16722  mhmmulg  16726  gsumwrev  16953  gsmsymgrfix  17005  gsmsymgreq  17009  psgnunilem3  17073  sylow1lem1  17186  efginvrel2  17313  efgsrel  17320  efgredlemd  17330  efgredlem  17333  efgred  17334  efgrelexlemb  17336  gsum2dlem2  17539  gsumcom2  17543  ablfac1eulem  17641  pgpfac1lem2  17644  pgpfac1lem5  17648  pgpfac1  17649  pgpfac  17653  srgmulgass  17700  srgpcomp  17701  srgbinom  17714  lmodvsmmulgdi  18062  isdomn2  18459  assamulgscm  18510  mplcoe1  18625  mplcoe3  18626  mplcoe5  18628  gsummoncoe1  18834  cnfldexp  18937  islindf4  19331  dmatval  19452  dmatel  19453  dmatmulcl  19460  pmatcoe1fsupp  19660  decpmataa0  19727  decpmatmulsumfsupp  19732  pmatcollpw2lem  19736  pm2mpmhmlem1  19777  fiinopn  19866  mretopd  20043  neiptoptop  20082  cnpfval  20185  iscnp3  20195  tgcn  20203  lmbr  20209  lmbr2  20210  lmbrf  20211  lmss  20249  ishaus  20273  hausnei2  20304  t1sep2  20320  fiuncmp  20354  dfcon2  20369  1stcfb  20395  2ndc1stc  20401  1stcrest  20403  1stcelcls  20411  1stccn  20413  lly1stc  20446  elkgen  20486  kgencn  20506  tx1stc  20600  xkopt  20605  cnmptcom  20628  isr0  20687  r0sep  20698  ptcmpfi  20763  isfildlem  20807  rnelfm  20903  fbflim  20926  flimrest  20933  isflf  20943  flffbas  20945  lmflf  20955  fclsrest  20974  isfcf  20984  cnextfvval  21015  tmdmulg  21042  tmdgsum  21045  eltsms  21082  tsmsi  21083  tsmsgsum  21088  tsmssubm  21092  tsmsres  21093  tsmsf1o  21094  isust  21153  isucn  21228  isucn2  21229  ucnima  21231  imasdsf1olem  21323  metss  21458  met1stc  21471  metcnp  21491  metcnpi  21494  metcnpi2  21495  metucn  21521  xrge0tsms  21787  fsumcn  21837  elcncf  21856  cncfi  21861  rescncf  21864  cncfco  21874  caucfil  22188  equivcau  22205  caubl  22212  caublcls  22213  ovolgelb  22368  ovolunlem1a  22384  ovolicc2lem3  22407  voliunlem1  22438  voliunlem3  22440  volsuplem  22443  volsup  22444  dyadmax  22491  vitali  22506  itg2leub  22627  itgfsum  22719  dvnadd  22818  dvnres  22820  cpnord  22824  dvnfre  22841  dvmptfsum  22862  dvferm1  22872  dvferm2  22874  rolle  22877  dvlip  22880  c1lip1  22884  lhop1  22901  deg1leb  22979  ply1divex  23022  fta1g  23053  plyco  23130  dgrcolem1  23162  dgrco  23164  dvnply2  23175  plydivex  23185  aalioulem2  23224  aalioulem3  23225  aalioulem5  23227  aaliou3lem2  23234  dvntaylp  23261  taylthlem1  23263  ulmdvlem3  23292  abelthlem9  23330  cxpmul2  23569  scvxcvx  23846  jensenlem2  23848  jensen  23849  wilthlem3  23930  perfectlem2  24093  bcmono  24140  bposlem5  24151  lgsquad2lem2  24222  dchrisumlem1  24262  dchrisum0flb  24283  pntpbnd1  24359  pntlemf  24378  qabvle  24398  qabvexp  24399  ostthlem2  24401  ostth2lem2  24407  tgcgr4  24511  sizeusglecusglem1  25147  2pthoncl  25268  fargshiftf1  25300  3v3e3cycl1  25307  4cycl4v4e  25329  4cycl4dv4e  25331  wlkiswwlk2lem4  25357  wlkiswwlk2  25360  clwlkisclwwlklem2a  25448  clwlkisclwwlklem2  25449  clwlkfoclwwlk  25508  el2wlkonot  25532  el2spthonot  25533  rusgranumwlk  25620  eupatrl  25631  eupath2  25643  frgra3vlem1  25663  3vfriswmgralem  25667  usg2spot2nb  25728  2spotmdisj  25731  numclwlk2lem2f1o  25768  isplig  25844  gxnn0add  25937  gxnn0mul  25940  ghgrpOLD  26031  ghabloOLD  26032  isnvlem  26164  nvi  26168  nmoubi  26348  nmounbi  26352  nmblolbi  26376  ipasslem1  26407  ipassi  26417  hlim2  26780  pjhth  26981  spansni  27145  elspansn2  27155  pjige0  27279  pjcjt2  27280  pjopyth  27308  elcnop  27445  elcnfn  27470  nmopub  27496  cnopc  27501  nmfnleub  27513  elnlfn  27516  cnfnc  27518  nmbdoplb  27613  nmcexi  27614  nmcoplb  27618  lnfnmul  27636  nmbdfnlb  27638  nmcfnlb  27642  pjss2coi  27752  pjssmi  27753  isst  27801  ishst  27802  stcltr1i  27862  mdbr  27882  dmdbr  27887  mddmd2  27897  mdslmd1lem3  27915  mdslmd1lem4  27916  elat2  27928  atcvat2  27977  cdj1i  28021  vtocl2d  28044  rmoeqALT  28058  iuninc  28115  fmptcof2  28198  nnindd  28327  nn0min  28328  isomnd  28408  omndadd  28413  isarchi2  28446  archirng  28449  archiexdiv  28451  archiabl  28459  xrge0tsmsd  28493  isorng  28507  ofldchr  28522  crefeq  28617  nexple  28776  esumfzf  28835  issiga  28878  isrnsiga  28880  isldsys  28923  ismeas  28966  isrnmeas  28967  measiun  28985  eulerpartlemn  29159  sseqp1  29173  rrvsum  29232  signsply0  29385  signstfvc  29408  bnj941  29529  bnj106  29624  bnj155  29635  bnj590  29666  bnj591  29667  bnj849  29681  bnj893  29684  bnj944  29694  bnj1128  29744  subfacp1lem6  29853  erdszelem8  29866  isscon  29894  cvmliftlem7  29959  cvmliftlem10  29962  cvmlift3lem2  29988  mrsubvrs  30105  mclsssvlem  30145  mclsval  30146  mclsax  30152  mclsind  30153  ghomf1olem  30257  shftvalg  30309  bccolsum  30319  iprodefisumlem  30320  faclimlem1  30323  dfpo2  30339  br1steqg  30360  br2ndeqg  30361  rdgprc  30385  trpredmintr  30416  frmin  30424  soseq  30436  frr3g  30457  fveleq  31053  bj-con3thALT  31097  bj-axc15v  31266  bj-axrep1  31310  bj-axrep2  31311  bj-axrep3  31312  rdgeqoa  31674  finxpreclem6  31689  wl-sblimt  31780  wl-sbhbt  31783  wl-2sb6d  31789  wl-mo2df  31800  wl-mo2t  31805  wl-ax12v3  31813  poimirlem2  31843  poimirlem25  31866  poimirlem28  31869  poimirlem31  31872  heicant  31876  mbfresfi  31888  itg2gt0cn  31898  sdclem2  31972  fdc  31975  seqpo  31977  incsequz  31978  mettrifi  31987  prdsbnd2  32028  heiborlem4  32047  bfplem1  32055  iscringd  32133  maxidlval  32173  igenval2  32200  ax12eq  32418  ax12el  32419  ax12indalem  32422  ax12inda2ALT  32423  ax12inda  32425  ax12v2-o  32426  riotasvd  32434  isopos  32652  isat3  32779  ishlat1  32824  glbconN  32848  ispsubsp  33216  isldil  33581  isltrn  33590  isdilN  33626  trlval  33634  cdleme27b  33841  cdleme29b  33848  cdleme31sn1  33854  cdleme31sn1c  33861  cdleme40v  33942  cdlemk36  34386  cdlemkid5  34408  cdlemn11pre  34684  dihord2pre  34699  islpolN  34957  hdmapffval  35303  hdmapfval  35304  hdmapval2lem  35308  ismrc  35449  incssnn0  35459  mzpexpmpt  35493  pell14qrexpclnn0  35619  monotuz  35696  expmordi  35702  rmxypos  35704  jm2.17a  35717  jm2.17b  35718  rmygeid  35721  divalgmodcl  35749  jm2.18  35750  jm2.19lem3  35753  jm2.25  35761  jm2.15nn0  35765  jm2.16nn0  35766  wepwsolem  35807  aomclem8  35826  dfac11  35827  pwslnm  35859  lnr2i  35882  hbtlem5  35894  cnsrexpcl  35938  rngunsnply  35946  isdomn3  35988  ifpbi23  36023  elmapintrab  36089  elmapintab  36109  cnvcnvintabd  36113  eliunov2  36178  relexpxpnnidm  36202  relexpiidm  36203  relexpss1d  36204  iunrelexpmin1  36207  relexpmulnn  36208  iunrelexpmin2  36211  relexp0a  36215  trclimalb2  36225  dvgrat  36568  pm14.122b  36681  fnchoice  37260  fiiuncl  37316  wessf1ornlem  37357  fperiodmullem  37412  fmul01  37535  fmuldfeq  37538  climsuselem1  37563  climinff  37567  climinffOLD  37568  ellimcabssub0  37574  limcleqr  37602  addlimc  37606  0ellimcdiv  37607  limclner  37609  dvnmptdivc  37690  dvnmptconst  37693  dvnmul  37695  iblspltprt  37727  itgspltprt  37733  stoweidlem2  37739  stoweidlem3  37740  stoweidlem17  37754  stoweidlem19  37756  stoweidlem21  37758  stoweidlem26  37763  fourierdlem42  37889  fourierdlem42OLD  37890  issal  38033  ismea  38134  isome  38160  carageniuncllem1  38187  caratheodorylem1  38192  smonoord  38525  perfectALTVlem2  38651  2ffzoeq  38855  usgra2pth  39253  usgfis  39343  lmodvsmdi  39754  dmatALTval  39780  dmatALTbasel  39782  snlindsntor  39851  ldepsnlinc  39888  elbigo2r  39951  elbigolo1  39955