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  889  pm4.14dc  891  imimorbdc  897  pm5.6dc  927  ax11v2  1834  ax11v  1841  equs5or  1844  mo23  2086  nfabdw  2358  2gencl  2796  3gencl  2797  vtocl2gf  2826  vtocl3gf  2827  eqeu  2934  mo2icl  2943  euind  2951  reu7  2959  reuind  2969  sbctt  3056  sbcnestgf  3136  preq12bg  3804  elint  3881  elintrabg  3888  intab  3904  trss  4141  bm1.3ii  4155  pocl  4339  swopolem  4341  sowlin  4356  frforeq3  4383  frirrg  4386  frind  4388  reusv3  4496  regexmid  4572  ordsoexmid  4599  tfisi  4624  finds2  4638  nnregexmid  4658  vtoclr  4712  2optocl  4741  3optocl  4742  raliunxp  4808  resieq  4957  iss  4993  cnveqb  5126  iotaexab  5238  funmo  5274  fnbrfvb  5604  fvelimab  5620  fvmptssdm  5649  fmptco  5731  fnressn  5751  fressnfv  5752  isoselem  5870  isosolem  5874  ovg  6066  caovcan  6092  caovordig  6093  caovord  6099  f1o2ndf1  6295  poxp  6299  smoeq  6357  smores  6359  tfrlem1  6375  tfrlemi1  6399  tfrexlem  6401  tfri3  6434  oawordriexmid  6537  nnacl  6547  nnmcl  6548  nnacom  6551  nnaass  6552  nndi  6553  nnmass  6554  nnmsucr  6555  nnmcom  6556  nnsucsssuc  6559  nntri3or  6560  nnaordi  6575  nnaword  6578  nnmordi  6583  nnaordex  6595  2ecoptocl  6691  3ecoptocl  6692  th3qlem2  6706  xpdom2g  6900  findcard2  6959  findcard2s  6960  xpfi  7002  supeq1  7061  ordiso2  7110  updjud  7157  nnnninfeq  7203  exmidontriimlem4  7307  exmidontriim  7308  distrnq0  7543  addassnq0  7546  elinp  7558  prcdnql  7568  prcunqu  7569  prarloclem3  7581  caucvgpr  7766  caucvgprpr  7796  ltsosr  7848  caucvgsrlemcau  7877  caucvgsrlemgt1  7879  caucvgsrlemoffres  7884  pitonn  7932  axpre-ltwlin  7967  axcaucvglemres  7983  sup3exmid  9001  nnaddcl  9027  nnmulcl  9028  zaddcllempos  9380  zaddcllemneg  9382  prime  9442  peano5uzti  9451  uzind2  9455  zindd  9461  uzaddcl  9677  exfzdc  10333  infssuzex  10340  nninfdcex  10344  frec2uzltd  10512  frec2uzrdg  10518  frecuzrdgtcl  10521  frecuzrdgg  10525  frecuzrdgfunlem  10528  seq3val  10569  seqvalcd  10570  seq3clss  10580  seq3fveq2  10584  seqfveq2g  10586  seq3shft2  10590  seqshft2g  10591  monoord  10594  seq3split  10597  seqsplitg  10598  seq3caopr3  10600  seqcaopr3g  10601  seq3f1olemp  10624  seqf1oglem2a  10627  seqf1og  10630  seq3id3  10633  seq3id2  10635  seq3homo  10636  seq3z  10637  seqhomog  10639  seqfeq4g  10640  ser3ge0  10645  exp3vallem  10649  expcllem  10659  expap0  10678  mulexp  10687  expadd  10690  expmul  10693  leexp2r  10702  leexp1a  10703  bernneq  10769  modqexp  10775  nn0ltexp2  10818  apexp1  10827  facdiv  10847  faclbnd  10850  faclbnd6  10853  omgadd  10911  seq3coll  10951  shftvalg  11018  shftval4g  11019  cjexp  11075  resqrexlemover  11192  resqrexlemdecn  11194  resqrexlemlo  11195  resqrexlemcalc3  11198  absexp  11261  climshft  11486  climub  11526  climserle  11527  fsum2d  11617  fsumabs  11647  fsumiun  11659  binom  11666  bcxmas  11671  cvgratnnlemnexp  11706  cvgratnnlemmn  11707  clim2prod  11721  prodfap0  11727  prodfrecap  11728  fprodabs  11798  fprod2d  11805  demoivreALT  11956  dvdsfac  12042  bitsinv1  12144  bezoutlemstep  12189  bezoutlemmain  12190  bezoutlemex  12193  dfgcd2  12206  gcdmultiple  12212  rplpwr  12219  nn0seqcvgd  12234  alginv  12240  algcvga  12244  algfx  12245  isprm4  12312  prmind2  12313  prmdvdsexp  12341  prmfac1  12345  eulerthlemrprm  12422  eulerthlema  12423  reumodprminv  12447  pcmpt  12537  pcfac  12544  prmpwdvds  12549  ennnfoneleminc  12653  ennnfonelemkh  12654  ennnfonelemhf1o  12655  ennnfonelemhom  12657  nninfdclemlt  12693  gsumfzz  13197  mulgnnass  13363  mhmmulg  13369  gsumfzconst  13547  srgmulgass  13621  srgpcomp  13622  lmodvsmmulgdi  13955  cnfldexp  14209  gsumfzfsumlemm  14219  fiinopn  14324  cnpfval  14515  iscnp3  14523  cnprcl2k  14526  tgcn  14528  lmbr  14533  lmbr2  14534  lmbrf  14535  lmss  14566  cnmptcom  14618  metss  14814  metcnp  14832  metcnpi  14835  metcnpi2  14836  elcncf  14893  cncfi  14898  rescncf  14901  cncfco  14911  cdivcncfap  14924  ellimc3apf  14980  limcdifap  14982  limcmpted  14983  limcimo  14985  limcresi  14986  cnplimclemr  14989  limccoap  14998  dvmptfsum  15045  plycolemc  15078  rpcxpmul2  15233  perfectlem2  15320  lgsquad2lem2  15407  bdbm1.3ii  15621  bj-2inf  15668  bj-omtrans  15686  nninfalllem1  15739  nninfsellemdc  15741  nninfsellemqall  15746