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  1805  ax12v2  2056  axc14  2086  sbcom2OLD  2174  ax12eq  2264  ax12el  2265  ax12indalem  2268  ax12inda2ALT  2269  ax12inda  2271  ax12v2-o  2272  mo2  2287  moOLD  2327  2moOLDOLD  2384  2eu6OLD  2394  2gencl  3144  3gencl  3145  vtocl2gf  3173  vtocl3gf  3174  vtocl4g  3182  eqeu  3274  mo2icl  3282  euind  3290  reu7  3298  reuind  3307  sbctt  3402  sbcnestgf  3839  r19.36zv  3928  dedth2h  3992  dedth3h  3993  dedth4h  3994  preq12bg  4205  prel12g  4206  elint  4288  elintrabg  4295  intab  4312  trss  4549  axrep1  4559  axrep2  4560  axrep3  4561  bm1.3ii  4571  reusv3  4655  pocl  4807  swopolem  4809  solin  4823  freq1  4849  frminex  4859  vtoclr  5043  2optocl  5075  3optocl  5076  raliunxp  5140  resieq  5282  iss  5319  cnveqb  5460  funmo  5602  funimaexg  5663  fnbrfvb  5906  fvelimab  5921  fvmptss  5956  fmptco  6052  fprg  6068  fnressn  6071  fressnfv  6073  isoselem  6223  ovg  6423  caovcan  6461  caovordig  6462  caovord  6468  tfisi  6671  tfindsg  6673  tfinds2  6676  tfinds3  6677  dfom2  6680  elom  6681  findsg  6705  finds2  6706  f1o2ndf1  6888  poxp  6892  fnse  6897  smoeq  7018  smores  7020  smogt  7035  tfrlem1  7042  tfr3  7065  oaordi  7192  oeordi  7233  oeoa  7243  oeoe  7245  nnacl  7257  nnmcl  7258  nnecl  7259  nnacom  7263  nnaordi  7264  nnawordi  7267  nnaass  7268  nndi  7269  nnmass  7270  nnmsucr  7271  nnmcom  7272  nnmordi  7277  2ecoptocl  7399  3ecoptocl  7400  undifixp  7502  xpdom2g  7610  findcard2  7756  xpfi  7787  fnfi  7794  fodomfi  7795  finsschain  7823  marypha1lem  7889  marypha1  7890  supeq1  7901  ordiso2  7936  ordtypelem7  7945  wemaplem1  7967  inf3lem2  8042  inf3lem5  8045  infdiffi  8070  cantnfval2  8084  cantnfle  8086  cantnfp1lem3  8095  oemapval  8098  cantnflem1  8104  cantnf  8108  cantnfval2OLD  8114  cantnfleOLD  8116  cantnfp1lem3OLD  8121  cantnflem1OLD  8127  cantnfOLD  8130  wemapwe  8135  wemapweOLD  8136  cnfcom  8140  cnfcom3clem  8145  cnfcomOLD  8148  cnfcom3clemOLD  8153  tz9.1  8156  r1pwOLD  8260  cplem2  8304  karden  8309  infxpenc2lem2  8393  infxpenc2lem2OLD  8397  fseqenlem1  8401  dfac8clem  8409  alephinit  8472  dfac4  8499  dfac5lem5  8504  dfac2a  8506  dfac2  8507  dfacacn  8517  dfac12lem3  8521  kmlem2  8527  kmlem13  8538  ackbij1lem16  8611  sornom  8653  infpssrlem4  8682  fin23lem14  8709  fin23lem32  8720  fin23lem34  8722  fin23lem36  8724  isf32lem1  8729  isf32lem2  8730  axcc2lem  8812  axcc3  8814  axcclem  8833  zornn0g  8881  ttukeylem5  8889  ttukeylem6  8890  axrepnd  8965  axpowndlem3  8971  axpowndlem3OLD  8972  zfcndrep  8988  fpwwe2lem8  9011  pwfseqlem3  9034  wunr1om  9093  wunfi  9095  tskr1om  9141  ingru  9189  grudomon  9191  axgroth3  9205  axgroth4  9206  nqereu  9303  mulcanenq  9334  elnp  9361  elnpi  9362  prlem934  9407  infm3  10498  nnaddcl  10554  nnmulcl  10555  peano5uzi  10945  uzind2  10949  uzindOLD  10951  zindd  10958  eluzadd  11106  uzaddcl  11133  uzwo  11140  uzwoOLD  11141  indstr  11146  zmax  11175  xmulasslem  11473  xrsupsslem  11494  xrinfmsslem  11495  xrsupss  11496  xrinfmss  11497  flval2  11914  om2uzlti  12025  uzrdgfni  12033  rabssnn0fi  12059  mptnn0fsupp  12067  seqcl2  12089  seqfveq2  12093  seqshft2  12097  monoord  12101  seqsplit  12104  seqcaopr3  12106  seqf1olem2a  12109  seqf1o  12112  seqid2  12117  seqhomo  12118  ser1const  12127  expcllem  12141  expeq0  12160  mulexp  12169  expadd  12172  expmul  12175  leexp2r  12187  leexp1a  12188  bernneq  12256  modexp  12265  facdiv  12329  faclbnd  12332  faclbnd4lem4  12338  faclbnd6  12341  hashgadd  12409  hashxp  12454  hashmap  12455  hashf1lem2  12467  hashf1  12468  seqcoll  12474  wrdind  12661  wrd2ind  12662  swrdccatin12lem3  12674  cshweqrep  12748  2cshwcshw  12752  cjexp  12942  absexp  13096  rlim  13277  rlim2  13278  rlim0  13290  rlim0lt  13291  rlimi  13295  ello12r  13299  ello1mpt  13303  ello1d  13305  elo12r  13310  lo1o1  13314  o1lo1  13319  lo1res  13341  climshft  13358  o1compt  13369  rlimo1  13398  lo1add  13408  lo1mul  13409  rlimdiv  13427  climub  13443  climserle  13444  caucvgrlem  13454  caurcvgr  13455  iseraltlem2  13464  summolem2a  13496  sumss  13505  fsum2d  13545  fsumabs  13574  fsumrlim  13584  fsumo1  13585  fsumiun  13594  binom  13601  bcxmas  13606  climcndslem1  13620  climcndslem2  13621  cvgrat  13651  demoivreALT  13793  ruclem8  13827  ruclem9  13828  dvdsle  13886  dvdsfac  13896  divalglem7  13912  bitsinv1  13947  sadcadd  13963  sadadd2  13965  saddisjlem  13969  smuval2  13987  smupvallem  13988  smu01lem  13990  smupval  13993  smueqlem  13995  smumullem  13997  bezoutlem4  14034  gcdmultiple  14043  rplpwr  14049  nn0seqcvgd  14054  seq1st  14055  alginv  14059  algcvga  14063  algfx  14064  prmind2  14083  prmdvdsexp  14110  prmfac1  14114  reumodprminv  14184  pcmpt  14266  pcfac  14273  prmpwdvds  14277  prmreclem4  14292  vdwlem10  14363  ramval  14381  ramcl  14402  cshwrepswhash1  14441  prmlem1a  14446  imasleval  14792  ismre  14841  mreexexd  14899  lubprop  15469  lublecllem  15471  glbprop  15482  joinlem  15494  meetlem  15508  isglbd  15600  lubun  15606  poslubmo  15629  posglbmo  15630  poslubd  15631  mrcmndind  15807  frmdgsum  15853  mulgnnass  15970  mhmmulg  15974  gsumwrev  16196  gsmsymgrfix  16248  gsmsymgreq  16252  psgnunilem3  16317  sylow1lem1  16414  efginvrel2  16541  efgsrel  16548  efgredlemd  16558  efgredlem  16561  efgred  16562  efgrelexlemb  16564  gsum2dlem2  16789  gsum2dOLD  16791  gsumcom2  16794  ablfac1eulem  16913  pgpfac1lem2  16916  pgpfac1lem5  16920  pgpfac1  16921  pgpfac  16925  srgmulgass  16970  srgpcomp  16971  srgbinom  16984  lmodvsmmulgdi  17330  isdomn2  17719  assamulgscm  17770  mplcoe1  17898  mplcoe3  17899  mplcoe3OLD  17900  mplcoe5  17902  mplcoe2OLD  17904  gsummoncoe1  18117  cnfldexp  18222  islindf4  18640  dmatval  18761  dmatel  18762  dmatmulcl  18769  pmatcoe1fsupp  18969  decpmataa0  19036  decpmatmulsumfsupp  19041  pmatcollpw2lem  19045  pm2mpmhmlem1  19086  fiinopn  19177  mretopd  19359  neiptoptop  19398  cnpfval  19501  iscnp3  19511  tgcn  19519  lmbr  19525  lmbr2  19526  lmbrf  19527  lmss  19565  ishaus  19589  hausnei2  19620  t1sep2  19636  fiuncmp  19670  dfcon2  19686  1stcfb  19712  2ndc1stc  19718  1stcrest  19720  1stcelcls  19728  1stccn  19730  lly1stc  19763  elkgen  19772  kgencn  19792  tx1stc  19886  xkopt  19891  cnmptcom  19914  isr0  19973  r0sep  19984  ptcmpfi  20049  isfildlem  20093  rnelfm  20189  fbflim  20212  flimrest  20219  isflf  20229  flffbas  20231  lmflf  20241  fclsrest  20260  isfcf  20270  cnextfvval  20300  tmdmulg  20326  tmdgsum  20329  eltsms  20366  tsmsi  20367  tsmsgsum  20372  tsmsgsumOLD  20375  tsmssubm  20379  tsmsresOLD  20380  tsmsres  20381  tsmsf1o  20382  isust  20441  isucn  20516  isucn2  20517  ucnima  20519  imasdsf1olem  20611  metss  20746  met1stc  20759  metcnp  20779  metcnpi  20782  metcnpi2  20783  metucnOLD  20826  metucn  20827  xrge0tsms  21074  fsumcn  21109  elcncf  21128  cncfi  21133  rescncf  21136  cncfco  21146  caucfil  21457  equivcau  21474  caubl  21481  caublcls  21482  ovolgelb  21626  ovolunlem1a  21642  ovolicc2lem3  21665  voliunlem1  21695  voliunlem3  21697  volsuplem  21700  volsup  21701  dyadmax  21742  vitali  21757  itg2leub  21876  itgfsum  21968  dvnadd  22067  dvnres  22069  cpnord  22073  dvnfre  22090  dvmptfsum  22111  dvferm1  22121  dvferm2  22123  rolle  22126  dvlip  22129  c1lip1  22133  lhop1  22150  deg1leb  22230  ply1divex  22272  fta1g  22303  plyco  22373  dgrcolem1  22404  dgrco  22406  dvnply2  22417  plydivex  22427  aalioulem2  22463  aalioulem3  22464  aalioulem5  22466  aaliou3lem2  22473  dvntaylp  22500  taylthlem1  22502  ulmdvlem3  22531  abelthlem9  22569  cxpmul2  22798  scvxcvx  23043  jensenlem2  23045  jensen  23046  wilthlem3  23072  perfectlem2  23233  bcmono  23280  bposlem5  23291  lgsquad2lem2  23362  dchrisumlem1  23402  dchrisum0flb  23423  pntpbnd1  23499  pntlemf  23518  qabvle  23538  qabvexp  23539  ostthlem2  23541  ostth2lem2  23547  sizeusglecusglem1  24160  2pthoncl  24281  fargshiftf1  24313  3v3e3cycl1  24320  4cycl4v4e  24342  4cycl4dv4e  24344  wlkiswwlk2lem4  24370  wlkiswwlk2  24373  clwlkisclwwlklem2a  24461  clwlkisclwwlklem2  24462  clwlkfoclwwlk  24521  el2wlkonot  24545  el2spthonot  24546  rusgranumwlk  24633  eupatrl  24644  eupath2  24656  frgra3vlem1  24676  3vfriswmgralem  24680  usg2spot2nb  24742  2spotmdisj  24745  numclwlk2lem2f1o  24782  isplig  24855  gxnn0add  24952  gxnn0mul  24955  ghgrp  25046  ghablo  25047  isnvlem  25179  nvi  25183  nmoubi  25363  nmounbi  25367  nmblolbi  25391  ipasslem1  25422  ipassi  25432  hlim2  25785  pjhth  25987  spansni  26151  elspansn2  26161  pjige0  26285  pjcjt2  26286  pjopyth  26314  elcnop  26452  elcnfn  26477  nmopub  26503  cnopc  26508  nmfnleub  26520  elnlfn  26523  cnfnc  26525  nmbdoplb  26620  nmcexi  26621  nmcoplb  26625  lnfnmul  26643  nmbdfnlb  26645  nmcfnlb  26649  pjss2coi  26759  pjssmi  26760  isst  26808  ishst  26809  stcltr1i  26869  mdbr  26889  dmdbr  26894  mddmd2  26904  mdslmd1lem3  26922  mdslmd1lem4  26923  elat2  26935  atcvat2  26984  cdj1i  27028  rmoeq  27062  iuninc  27101  fmptcof2  27174  nn0indd  27277  nn0min  27279  isomnd  27353  omndadd  27358  isarchi2  27391  archirng  27394  archiexdiv  27396  archiabl  27404  xrge0tsmsd  27438  isorng  27452  ofldchr  27467  nexple  27645  esumfzf  27715  issiga  27751  isrnsiga  27753  ismeas  27810  isrnmeas  27811  measiun  27829  eulerpartlemn  27960  sseqp1  27974  rrvsum  28033  signsply0  28148  signstfvc  28171  subfacp1lem6  28269  erdszelem8  28282  isscon  28311  cvmliftlem7  28376  cvmliftlem10  28379  cvmlift3lem2  28405  ghomf1olem  28509  relexp0  28527  relexpsucr  28528  relexpsucl  28530  relexpind  28538  dfrtrclrec2  28541  rtrclreclem.refl  28542  rtrclreclem.subset  28543  rtrclreclem.min  28545  dfrtrcl2  28546  shftvalg  28591  clim2prod  28599  prodfn0  28605  prodfrec  28606  ntrivcvgfvn0  28610  prodmolem2a  28643  fprodabs  28680  fprodefsum  28681  fprodn0  28686  fprod2d  28688  iprodefisumlem  28700  binomfallfac  28740  faclimlem1  28745  dfpo2  28761  rdgprc  28804  preddowncl  28853  trpredmintr  28891  frmin  28899  soseq  28911  wfr3g  28919  wfrlem4  28923  frr3g  28963  bpolycl  29391  bpolydif  29394  fveleq  29493  wl-sblimt  29576  wl-sbhbt  29579  wl-2sb6d  29585  wl-mo2dnae  29596  wl-mo2t  29597  heicant  29626  mbfresfi  29638  itg2gt0cn  29647  sdclem2  29838  fdc  29841  seqpo  29843  incsequz  29844  mettrifi  29853  prdsbnd2  29894  heiborlem4  29913  bfplem1  29921  iscringd  29999  maxidlval  30039  igenval2  30066  ismrc  30237  incssnn0  30247  mzpexpmpt  30281  pell14qrexpclnn0  30406  monotuz  30481  expmordi  30487  rmxypos  30489  jm2.17a  30502  jm2.17b  30503  rmygeid  30506  divalgmodcl  30533  jm2.18  30534  jm2.19lem3  30537  jm2.25  30545  jm2.15nn0  30549  jm2.16nn0  30550  wepwsolem  30591  aomclem8  30611  dfac11  30612  pwslnm  30644  lnr2i  30669  hbtlem5  30681  cnsrexpcl  30719  rngunsnply  30727  isdomn3  30769  pm14.122b  30908  fnchoice  30982  fperiodmullem  31080  fmul01  31130  fmuldfeq  31133  climsuselem1  31149  climinff  31153  ellimcabssub0  31159  limcleqr  31186  addlimc  31190  0ellimcdiv  31191  limclner  31193  iblspltprt  31291  itgspltprt  31297  stoweidlem2  31302  stoweidlem3  31303  stoweidlem17  31317  stoweidlem19  31319  stoweidlem21  31321  stoweidlem26  31326  fourierdlem42  31449  2ffzoeq  31810  usgra2pth  31823  usgfis  31915  lmodvsmdi  32048  dmatALTval  32074  dmatALTbasel  32076  snlindsntor  32145  ldepsnlinc  32190  bnj941  32910  bnj106  33005  bnj155  33016  bnj590  33047  bnj591  33048  bnj849  33062  bnj893  33065  bnj944  33075  bnj1128  33125  bj-con3ALT  33242  bj-axc15v  33411  bj-axrep1  33455  bj-axrep2  33456  bj-axrep3  33457  riotasvd  33759  isopos  33977  isat3  34104  ishlat1  34149  glbconN  34173  ispsubsp  34541  isldil  34906  isltrn  34915  isdilN  34950  trlval  34958  cdleme27b  35164  cdleme29b  35171  cdleme31sn1  35177  cdleme31sn1c  35184  cdleme40v  35265  cdlemk36  35709  cdlemkid5  35731  cdlemn11pre  36007  dihord2pre  36022  islpolN  36280  hdmapffval  36626  hdmapfval  36627  hdmapval2lem  36631