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  896  pm4.14dc  898  imimorbdc  904  pm5.6dc  934  ax11v2  1869  ax11v  1876  equs5or  1879  mo23  2122  nfabdw  2403  2gencl  2847  3gencl  2848  vtocl2gf  2877  vtocl3gf  2878  vtocl4g  2886  vtocl4ga  2887  eqeu  2987  mo2icl  2996  euind  3004  reu7  3012  reuind  3022  sbctt  3109  reu8nf  3124  sbcnestgf  3190  preq12bg  3877  elint  3955  elintrabg  3962  intab  3978  trss  4217  bm1.3ii  4231  pocl  4424  swopolem  4426  sowlin  4441  frforeq3  4468  frirrg  4471  frind  4473  reusv3  4581  regexmid  4657  ordsoexmid  4684  tfisi  4709  finds2  4723  nnregexmid  4743  vtoclr  4798  2optocl  4827  3optocl  4828  raliunxp  4896  resieq  5048  iss  5084  cnveqb  5218  iotaexab  5331  funmo  5367  fnbrfvb  5715  fvelimab  5733  fvmptssdm  5762  fmptco  5843  fnressn  5870  fressnfv  5871  isoselem  5993  isosolem  5997  ovg  6193  caovcan  6219  caovordig  6220  caovord  6226  f1o2ndf1  6424  poxp  6428  smoeq  6521  smores  6523  tfrlem1  6539  tfrlemi1  6563  tfrexlem  6565  tfri3  6598  oawordriexmid  6703  nnacl  6713  nnmcl  6714  nnacom  6717  nnaass  6718  nndi  6719  nnmass  6720  nnmsucr  6721  nnmcom  6722  nnsucsssuc  6725  nntri3or  6726  nnaordi  6741  nnaword  6744  nnmordi  6749  nnaordex  6761  2ecoptocl  6857  3ecoptocl  6858  th3qlem2  6872  xpdom2g  7083  findcard2  7146  findcard2s  7147  xpfi  7192  supeq1  7277  ordiso2  7326  updjud  7373  nnnninfeq  7419  exmidontriimlem4  7531  exmidontriim  7532  papcotr  7562  distrnq0  7774  addassnq0  7777  elinp  7789  prcdnql  7799  prcunqu  7800  prarloclem3  7812  caucvgpr  7997  caucvgprpr  8027  ltsosr  8079  caucvgsrlemcau  8108  caucvgsrlemgt1  8110  caucvgsrlemoffres  8115  pitonn  8163  axpre-ltwlin  8198  axcaucvglemres  8214  sup3exmid  9231  nnaddcl  9257  nnmulcl  9258  zaddcllempos  9614  zaddcllemneg  9616  prime  9677  peano5uzti  9686  uzind2  9690  zindd  9696  uzaddcl  9918  exfzdc  10586  infssuzex  10593  nninfdcex  10597  frec2uzltd  10765  frec2uzrdg  10771  frecuzrdgtcl  10774  frecuzrdgg  10778  frecuzrdgfunlem  10781  seq3val  10822  seqvalcd  10823  seq3clss  10833  seq3fveq2  10837  seqfveq2g  10839  seq3shft2  10843  seqshft2g  10844  monoord  10847  seq3split  10850  seqsplitg  10851  seq3caopr3  10853  seqcaopr3g  10854  seq3f1olemp  10877  seqf1oglem2a  10880  seqf1og  10883  seq3id3  10886  seq3id2  10888  seq3homo  10889  seq3z  10890  seqhomog  10892  seqfeq4g  10893  ser3ge0  10898  exp3vallem  10902  expcllem  10912  expap0  10931  mulexp  10940  expadd  10943  expmul  10946  leexp2r  10955  leexp1a  10956  bernneq  11022  modqexp  11028  nn0ltexp2  11071  apexp1  11080  facdiv  11100  faclbnd  11103  faclbnd6  11106  omgadd  11166  hashmap  11192  seq3coll  11214  wrdind  11414  wrd2ind  11415  pfxccatin12lem3  11424  shftvalg  11521  shftval4g  11522  cjexp  11578  resqrexlemover  11695  resqrexlemdecn  11697  resqrexlemlo  11698  resqrexlemcalc3  11701  absexp  11764  climshft  11989  climub  12029  climserle  12030  fsum2d  12121  fsumabs  12151  fsumiun  12163  binom  12170  bcxmas  12175  cvgratnnlemnexp  12210  cvgratnnlemmn  12211  clim2prod  12225  prodfap0  12231  prodfrecap  12232  fprodabs  12302  fprod2d  12309  demoivreALT  12460  dvdsfac  12546  bitsinv1  12648  bezoutlemstep  12693  bezoutlemmain  12694  bezoutlemex  12697  dfgcd2  12710  gcdmultiple  12716  rplpwr  12723  nn0seqcvgd  12738  alginv  12744  algcvga  12748  algfx  12749  isprm4  12816  prmind2  12817  prmdvdsexp  12845  prmfac1  12849  eulerthlemrprm  12926  eulerthlema  12927  reumodprminv  12951  pcmpt  13041  pcfac  13048  prmpwdvds  13053  ennnfoneleminc  13162  ennnfonelemkh  13163  ennnfonelemhf1o  13164  ennnfonelemhom  13166  nninfdclemlt  13202  gsumfzz  13708  mulgnnass  13874  mhmmulg  13880  gsumfzconst  14058  srgmulgass  14133  srgpcomp  14134  lmodvsmmulgdi  14471  cnfldexp  14725  gsumfzfsumlemm  14735  mplelbascoe  14847  fiinopn  14869  cnpfval  15060  iscnp3  15068  cnprcl2k  15071  tgcn  15073  lmbr  15078  lmbr2  15079  lmbrf  15080  lmss  15111  cnmptcom  15163  metss  15359  metcnp  15377  metcnpi  15380  metcnpi2  15381  elcncf  15438  cncfi  15443  rescncf  15446  cncfco  15456  cdivcncfap  15469  ellimc3apf  15525  limcdifap  15527  limcmpted  15528  limcimo  15530  limcresi  15531  cnplimclemr  15534  limccoap  15543  dvmptfsum  15590  plycolemc  15623  rpcxpmul2  15778  perfectlem2  15868  lgsquad2lem2  15955  eupth2fi  16474  depindlem2  16502  depindlem3  16503  bdbm1.3ii  16661  bj-2inf  16708  bj-omtrans  16726  exmidcon  16780  exmidpeirce  16781  nninfalllem1  16786  nninfsellemdc  16788  nninfsellemqall  16793