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  893  pm4.14dc  895  imimorbdc  901  pm5.6dc  931  ax11v2  1866  ax11v  1873  equs5or  1876  mo23  2119  nfabdw  2391  2gencl  2833  3gencl  2834  vtocl2gf  2863  vtocl3gf  2864  vtocl4g  2872  vtocl4ga  2873  eqeu  2973  mo2icl  2982  euind  2990  reu7  2998  reuind  3008  sbctt  3095  reu8nf  3110  sbcnestgf  3176  preq12bg  3851  elint  3929  elintrabg  3936  intab  3952  trss  4191  bm1.3ii  4205  pocl  4394  swopolem  4396  sowlin  4411  frforeq3  4438  frirrg  4441  frind  4443  reusv3  4551  regexmid  4627  ordsoexmid  4654  tfisi  4679  finds2  4693  nnregexmid  4713  vtoclr  4767  2optocl  4796  3optocl  4797  raliunxp  4863  resieq  5015  iss  5051  cnveqb  5184  iotaexab  5297  funmo  5333  fnbrfvb  5672  fvelimab  5690  fvmptssdm  5719  fmptco  5801  fnressn  5825  fressnfv  5826  isoselem  5944  isosolem  5948  ovg  6144  caovcan  6170  caovordig  6171  caovord  6177  f1o2ndf1  6374  poxp  6378  smoeq  6436  smores  6438  tfrlem1  6454  tfrlemi1  6478  tfrexlem  6480  tfri3  6513  oawordriexmid  6616  nnacl  6626  nnmcl  6627  nnacom  6630  nnaass  6631  nndi  6632  nnmass  6633  nnmsucr  6634  nnmcom  6635  nnsucsssuc  6638  nntri3or  6639  nnaordi  6654  nnaword  6657  nnmordi  6662  nnaordex  6674  2ecoptocl  6770  3ecoptocl  6771  th3qlem2  6785  xpdom2g  6991  findcard2  7051  findcard2s  7052  xpfi  7094  supeq1  7153  ordiso2  7202  updjud  7249  nnnninfeq  7295  exmidontriimlem4  7406  exmidontriim  7407  distrnq0  7646  addassnq0  7649  elinp  7661  prcdnql  7671  prcunqu  7672  prarloclem3  7684  caucvgpr  7869  caucvgprpr  7899  ltsosr  7951  caucvgsrlemcau  7980  caucvgsrlemgt1  7982  caucvgsrlemoffres  7987  pitonn  8035  axpre-ltwlin  8070  axcaucvglemres  8086  sup3exmid  9104  nnaddcl  9130  nnmulcl  9131  zaddcllempos  9483  zaddcllemneg  9485  prime  9546  peano5uzti  9555  uzind2  9559  zindd  9565  uzaddcl  9781  exfzdc  10446  infssuzex  10453  nninfdcex  10457  frec2uzltd  10625  frec2uzrdg  10631  frecuzrdgtcl  10634  frecuzrdgg  10638  frecuzrdgfunlem  10641  seq3val  10682  seqvalcd  10683  seq3clss  10693  seq3fveq2  10697  seqfveq2g  10699  seq3shft2  10703  seqshft2g  10704  monoord  10707  seq3split  10710  seqsplitg  10711  seq3caopr3  10713  seqcaopr3g  10714  seq3f1olemp  10737  seqf1oglem2a  10740  seqf1og  10743  seq3id3  10746  seq3id2  10748  seq3homo  10749  seq3z  10750  seqhomog  10752  seqfeq4g  10753  ser3ge0  10758  exp3vallem  10762  expcllem  10772  expap0  10791  mulexp  10800  expadd  10803  expmul  10806  leexp2r  10815  leexp1a  10816  bernneq  10882  modqexp  10888  nn0ltexp2  10931  apexp1  10940  facdiv  10960  faclbnd  10963  faclbnd6  10966  omgadd  11024  seq3coll  11064  wrdind  11254  wrd2ind  11255  pfxccatin12lem3  11264  shftvalg  11347  shftval4g  11348  cjexp  11404  resqrexlemover  11521  resqrexlemdecn  11523  resqrexlemlo  11524  resqrexlemcalc3  11527  absexp  11590  climshft  11815  climub  11855  climserle  11856  fsum2d  11946  fsumabs  11976  fsumiun  11988  binom  11995  bcxmas  12000  cvgratnnlemnexp  12035  cvgratnnlemmn  12036  clim2prod  12050  prodfap0  12056  prodfrecap  12057  fprodabs  12127  fprod2d  12134  demoivreALT  12285  dvdsfac  12371  bitsinv1  12473  bezoutlemstep  12518  bezoutlemmain  12519  bezoutlemex  12522  dfgcd2  12535  gcdmultiple  12541  rplpwr  12548  nn0seqcvgd  12563  alginv  12569  algcvga  12573  algfx  12574  isprm4  12641  prmind2  12642  prmdvdsexp  12670  prmfac1  12674  eulerthlemrprm  12751  eulerthlema  12752  reumodprminv  12776  pcmpt  12866  pcfac  12873  prmpwdvds  12878  ennnfoneleminc  12982  ennnfonelemkh  12983  ennnfonelemhf1o  12984  ennnfonelemhom  12986  nninfdclemlt  13022  gsumfzz  13528  mulgnnass  13694  mhmmulg  13700  gsumfzconst  13878  srgmulgass  13952  srgpcomp  13953  lmodvsmmulgdi  14287  cnfldexp  14541  gsumfzfsumlemm  14551  mplelbascoe  14656  fiinopn  14678  cnpfval  14869  iscnp3  14877  cnprcl2k  14880  tgcn  14882  lmbr  14887  lmbr2  14888  lmbrf  14889  lmss  14920  cnmptcom  14972  metss  15168  metcnp  15186  metcnpi  15189  metcnpi2  15190  elcncf  15247  cncfi  15252  rescncf  15255  cncfco  15265  cdivcncfap  15278  ellimc3apf  15334  limcdifap  15336  limcmpted  15337  limcimo  15339  limcresi  15340  cnplimclemr  15343  limccoap  15352  dvmptfsum  15399  plycolemc  15432  rpcxpmul2  15587  perfectlem2  15674  lgsquad2lem2  15761  bdbm1.3ii  16254  bj-2inf  16301  bj-omtrans  16319  nninfalllem1  16374  nninfsellemdc  16376  nninfsellemqall  16381