Theorem imbi2d 230

Description: Deduction adding an antecedent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-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 22	. 2 |- ( ph -> ( th -> ( ps <-> ch ) ) )
3	2	pm5.74d 182	1 |- ( ph -> ( ( th -> ps ) <-> ( th -> ch ) ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  imbi12d  234  imbi2  237  pm5.42  320  imanst  888  pm4.14dc  890  imimorbdc  896  pm5.6dc  926  ax11v2  1820  ax11v  1827  equs5or  1830  mo23  2067  nfabdw  2338  2gencl  2771  3gencl  2772  vtocl2gf  2800  vtocl3gf  2801  eqeu  2908  mo2icl  2917  euind  2925  reu7  2933  reuind  2943  sbctt  3030  sbcnestgf  3109  preq12bg  3774  elint  3851  elintrabg  3858  intab  3874  trss  4111  bm1.3ii  4125  pocl  4304  swopolem  4306  sowlin  4321  frforeq3  4348  frirrg  4351  frind  4353  reusv3  4461  regexmid  4535  ordsoexmid  4562  tfisi  4587  finds2  4601  nnregexmid  4621  vtoclr  4675  2optocl  4704  3optocl  4705  raliunxp  4769  resieq  4918  iss  4954  cnveqb  5085  funmo  5232  fnbrfvb  5557  fvelimab  5573  fvmptssdm  5601  fmptco  5683  fnressn  5703  fressnfv  5704  isoselem  5821  isosolem  5825  ovg  6013  caovcan  6039  caovordig  6040  caovord  6046  f1o2ndf1  6229  poxp  6233  smoeq  6291  smores  6293  tfrlem1  6309  tfrlemi1  6333  tfrexlem  6335  tfri3  6368  oawordriexmid  6471  nnacl  6481  nnmcl  6482  nnacom  6485  nnaass  6486  nndi  6487  nnmass  6488  nnmsucr  6489  nnmcom  6490  nnsucsssuc  6493  nntri3or  6494  nnaordi  6509  nnaword  6512  nnmordi  6517  nnaordex  6529  2ecoptocl  6623  3ecoptocl  6624  th3qlem2  6638  xpdom2g  6832  findcard2  6889  findcard2s  6890  xpfi  6929  supeq1  6985  ordiso2  7034  updjud  7081  nnnninfeq  7126  exmidontriimlem4  7223  exmidontriim  7224  distrnq0  7458  addassnq0  7461  elinp  7473  prcdnql  7483  prcunqu  7484  prarloclem3  7496  caucvgpr  7681  caucvgprpr  7711  ltsosr  7763  caucvgsrlemcau  7792  caucvgsrlemgt1  7794  caucvgsrlemoffres  7799  pitonn  7847  axpre-ltwlin  7882  axcaucvglemres  7898  sup3exmid  8914  nnaddcl  8939  nnmulcl  8940  zaddcllempos  9290  zaddcllemneg  9292  prime  9352  peano5uzti  9361  uzind2  9365  zindd  9371  uzaddcl  9586  exfzdc  10240  frec2uzltd  10403  frec2uzrdg  10409  frecuzrdgtcl  10412  frecuzrdgg  10416  frecuzrdgfunlem  10419  seq3val  10458  seqvalcd  10459  seq3clss  10467  seq3fveq2  10469  seq3shft2  10473  monoord  10476  seq3split  10479  seq3caopr3  10481  seq3f1olemp  10502  seq3id3  10507  seq3id2  10509  seq3homo  10510  seq3z  10511  ser3ge0  10517  exp3vallem  10521  expcllem  10531  expap0  10550  mulexp  10559  expadd  10562  expmul  10565  leexp2r  10574  leexp1a  10575  bernneq  10641  modqexp  10647  nn0ltexp2  10689  apexp1  10698  facdiv  10718  faclbnd  10721  faclbnd6  10724  omgadd  10782  seq3coll  10822  shftvalg  10845  shftval4g  10846  cjexp  10902  resqrexlemover  11019  resqrexlemdecn  11021  resqrexlemlo  11022  resqrexlemcalc3  11025  absexp  11088  climshft  11312  climub  11352  climserle  11353  fsum2d  11443  fsumabs  11473  fsumiun  11485  binom  11492  bcxmas  11497  cvgratnnlemnexp  11532  cvgratnnlemmn  11533  clim2prod  11547  prodfap0  11553  prodfrecap  11554  fprodabs  11624  fprod2d  11631  demoivreALT  11781  dvdsfac  11866  infssuzex  11950  nninfdcex  11954  bezoutlemstep  11998  bezoutlemmain  11999  bezoutlemex  12002  dfgcd2  12015  gcdmultiple  12021  rplpwr  12028  nn0seqcvgd  12041  alginv  12047  algcvga  12051  algfx  12052  isprm4  12119  prmind2  12120  prmdvdsexp  12148  prmfac1  12152  eulerthlemrprm  12229  eulerthlema  12230  reumodprminv  12253  pcmpt  12341  pcfac  12348  prmpwdvds  12353  ennnfoneleminc  12412  ennnfonelemkh  12413  ennnfonelemhf1o  12414  ennnfonelemhom  12416  nninfdclemlt  12452  mulgnnass  13018  mhmmulg  13024  srgmulgass  13172  srgpcomp  13173  lmodvsmmulgdi  13413  cnfldexp  13474  fiinopn  13507  cnpfval  13698  iscnp3  13706  cnprcl2k  13709  tgcn  13711  lmbr  13716  lmbr2  13717  lmbrf  13718  lmss  13749  cnmptcom  13801  metss  13997  metcnp  14015  metcnpi  14018  metcnpi2  14019  elcncf  14063  cncfi  14068  rescncf  14071  cncfco  14081  cdivcncfap  14090  ellimc3apf  14132  limcdifap  14134  limcmpted  14135  limcimo  14137  limcresi  14138  cnplimclemr  14141  limccoap  14150  bdbm1.3ii  14646  bj-2inf  14693  bj-omtrans  14711  nninfalllem1  14760  nninfsellemdc  14762  nninfsellemqall  14767