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  5674  fvelimab  5692  fvmptssdm  5721  fmptco  5803  fnressn  5829  fressnfv  5830  isoselem  5950  isosolem  5954  ovg  6150  caovcan  6176  caovordig  6177  caovord  6183  f1o2ndf1  6380  poxp  6384  smoeq  6442  smores  6444  tfrlem1  6460  tfrlemi1  6484  tfrexlem  6486  tfri3  6519  oawordriexmid  6624  nnacl  6634  nnmcl  6635  nnacom  6638  nnaass  6639  nndi  6640  nnmass  6641  nnmsucr  6642  nnmcom  6643  nnsucsssuc  6646  nntri3or  6647  nnaordi  6662  nnaword  6665  nnmordi  6670  nnaordex  6682  2ecoptocl  6778  3ecoptocl  6779  th3qlem2  6793  xpdom2g  6999  findcard2  7059  findcard2s  7060  xpfi  7105  supeq1  7164  ordiso2  7213  updjud  7260  nnnninfeq  7306  exmidontriimlem4  7417  exmidontriim  7418  distrnq0  7657  addassnq0  7660  elinp  7672  prcdnql  7682  prcunqu  7683  prarloclem3  7695  caucvgpr  7880  caucvgprpr  7910  ltsosr  7962  caucvgsrlemcau  7991  caucvgsrlemgt1  7993  caucvgsrlemoffres  7998  pitonn  8046  axpre-ltwlin  8081  axcaucvglemres  8097  sup3exmid  9115  nnaddcl  9141  nnmulcl  9142  zaddcllempos  9494  zaddcllemneg  9496  prime  9557  peano5uzti  9566  uzind2  9570  zindd  9576  uzaddcl  9793  exfzdc  10458  infssuzex  10465  nninfdcex  10469  frec2uzltd  10637  frec2uzrdg  10643  frecuzrdgtcl  10646  frecuzrdgg  10650  frecuzrdgfunlem  10653  seq3val  10694  seqvalcd  10695  seq3clss  10705  seq3fveq2  10709  seqfveq2g  10711  seq3shft2  10715  seqshft2g  10716  monoord  10719  seq3split  10722  seqsplitg  10723  seq3caopr3  10725  seqcaopr3g  10726  seq3f1olemp  10749  seqf1oglem2a  10752  seqf1og  10755  seq3id3  10758  seq3id2  10760  seq3homo  10761  seq3z  10762  seqhomog  10764  seqfeq4g  10765  ser3ge0  10770  exp3vallem  10774  expcllem  10784  expap0  10803  mulexp  10812  expadd  10815  expmul  10818  leexp2r  10827  leexp1a  10828  bernneq  10894  modqexp  10900  nn0ltexp2  10943  apexp1  10952  facdiv  10972  faclbnd  10975  faclbnd6  10978  omgadd  11036  seq3coll  11077  wrdind  11270  wrd2ind  11271  pfxccatin12lem3  11280  shftvalg  11363  shftval4g  11364  cjexp  11420  resqrexlemover  11537  resqrexlemdecn  11539  resqrexlemlo  11540  resqrexlemcalc3  11543  absexp  11606  climshft  11831  climub  11871  climserle  11872  fsum2d  11962  fsumabs  11992  fsumiun  12004  binom  12011  bcxmas  12016  cvgratnnlemnexp  12051  cvgratnnlemmn  12052  clim2prod  12066  prodfap0  12072  prodfrecap  12073  fprodabs  12143  fprod2d  12150  demoivreALT  12301  dvdsfac  12387  bitsinv1  12489  bezoutlemstep  12534  bezoutlemmain  12535  bezoutlemex  12538  dfgcd2  12551  gcdmultiple  12557  rplpwr  12564  nn0seqcvgd  12579  alginv  12585  algcvga  12589  algfx  12590  isprm4  12657  prmind2  12658  prmdvdsexp  12686  prmfac1  12690  eulerthlemrprm  12767  eulerthlema  12768  reumodprminv  12792  pcmpt  12882  pcfac  12889  prmpwdvds  12894  ennnfoneleminc  12998  ennnfonelemkh  12999  ennnfonelemhf1o  13000  ennnfonelemhom  13002  nninfdclemlt  13038  gsumfzz  13544  mulgnnass  13710  mhmmulg  13716  gsumfzconst  13894  srgmulgass  13968  srgpcomp  13969  lmodvsmmulgdi  14303  cnfldexp  14557  gsumfzfsumlemm  14567  mplelbascoe  14672  fiinopn  14694  cnpfval  14885  iscnp3  14893  cnprcl2k  14896  tgcn  14898  lmbr  14903  lmbr2  14904  lmbrf  14905  lmss  14936  cnmptcom  14988  metss  15184  metcnp  15202  metcnpi  15205  metcnpi2  15206  elcncf  15263  cncfi  15268  rescncf  15271  cncfco  15281  cdivcncfap  15294  ellimc3apf  15350  limcdifap  15352  limcmpted  15353  limcimo  15355  limcresi  15356  cnplimclemr  15359  limccoap  15368  dvmptfsum  15415  plycolemc  15448  rpcxpmul2  15603  perfectlem2  15690  lgsquad2lem2  15777  bdbm1.3ii  16337  bj-2inf  16384  bj-omtrans  16402  nninfalllem1  16462  nninfsellemdc  16464  nninfsellemqall  16469