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  890  pm4.14dc  892  imimorbdc  898  pm5.6dc  928  ax11v2  1843  ax11v  1850  equs5or  1853  mo23  2095  nfabdw  2367  2gencl  2805  3gencl  2806  vtocl2gf  2835  vtocl3gf  2836  eqeu  2943  mo2icl  2952  euind  2960  reu7  2968  reuind  2978  sbctt  3065  sbcnestgf  3145  preq12bg  3814  elint  3891  elintrabg  3898  intab  3914  trss  4151  bm1.3ii  4165  pocl  4350  swopolem  4352  sowlin  4367  frforeq3  4394  frirrg  4397  frind  4399  reusv3  4507  regexmid  4583  ordsoexmid  4610  tfisi  4635  finds2  4649  nnregexmid  4669  vtoclr  4723  2optocl  4752  3optocl  4753  raliunxp  4819  resieq  4969  iss  5005  cnveqb  5138  iotaexab  5250  funmo  5286  fnbrfvb  5619  fvelimab  5635  fvmptssdm  5664  fmptco  5746  fnressn  5770  fressnfv  5771  isoselem  5889  isosolem  5893  ovg  6085  caovcan  6111  caovordig  6112  caovord  6118  f1o2ndf1  6314  poxp  6318  smoeq  6376  smores  6378  tfrlem1  6394  tfrlemi1  6418  tfrexlem  6420  tfri3  6453  oawordriexmid  6556  nnacl  6566  nnmcl  6567  nnacom  6570  nnaass  6571  nndi  6572  nnmass  6573  nnmsucr  6574  nnmcom  6575  nnsucsssuc  6578  nntri3or  6579  nnaordi  6594  nnaword  6597  nnmordi  6602  nnaordex  6614  2ecoptocl  6710  3ecoptocl  6711  th3qlem2  6725  xpdom2g  6927  findcard2  6986  findcard2s  6987  xpfi  7029  supeq1  7088  ordiso2  7137  updjud  7184  nnnninfeq  7230  exmidontriimlem4  7336  exmidontriim  7337  distrnq0  7572  addassnq0  7575  elinp  7587  prcdnql  7597  prcunqu  7598  prarloclem3  7610  caucvgpr  7795  caucvgprpr  7825  ltsosr  7877  caucvgsrlemcau  7906  caucvgsrlemgt1  7908  caucvgsrlemoffres  7913  pitonn  7961  axpre-ltwlin  7996  axcaucvglemres  8012  sup3exmid  9030  nnaddcl  9056  nnmulcl  9057  zaddcllempos  9409  zaddcllemneg  9411  prime  9472  peano5uzti  9481  uzind2  9485  zindd  9491  uzaddcl  9707  exfzdc  10369  infssuzex  10376  nninfdcex  10380  frec2uzltd  10548  frec2uzrdg  10554  frecuzrdgtcl  10557  frecuzrdgg  10561  frecuzrdgfunlem  10564  seq3val  10605  seqvalcd  10606  seq3clss  10616  seq3fveq2  10620  seqfveq2g  10622  seq3shft2  10626  seqshft2g  10627  monoord  10630  seq3split  10633  seqsplitg  10634  seq3caopr3  10636  seqcaopr3g  10637  seq3f1olemp  10660  seqf1oglem2a  10663  seqf1og  10666  seq3id3  10669  seq3id2  10671  seq3homo  10672  seq3z  10673  seqhomog  10675  seqfeq4g  10676  ser3ge0  10681  exp3vallem  10685  expcllem  10695  expap0  10714  mulexp  10723  expadd  10726  expmul  10729  leexp2r  10738  leexp1a  10739  bernneq  10805  modqexp  10811  nn0ltexp2  10854  apexp1  10863  facdiv  10883  faclbnd  10886  faclbnd6  10889  omgadd  10947  seq3coll  10987  shftvalg  11147  shftval4g  11148  cjexp  11204  resqrexlemover  11321  resqrexlemdecn  11323  resqrexlemlo  11324  resqrexlemcalc3  11327  absexp  11390  climshft  11615  climub  11655  climserle  11656  fsum2d  11746  fsumabs  11776  fsumiun  11788  binom  11795  bcxmas  11800  cvgratnnlemnexp  11835  cvgratnnlemmn  11836  clim2prod  11850  prodfap0  11856  prodfrecap  11857  fprodabs  11927  fprod2d  11934  demoivreALT  12085  dvdsfac  12171  bitsinv1  12273  bezoutlemstep  12318  bezoutlemmain  12319  bezoutlemex  12322  dfgcd2  12335  gcdmultiple  12341  rplpwr  12348  nn0seqcvgd  12363  alginv  12369  algcvga  12373  algfx  12374  isprm4  12441  prmind2  12442  prmdvdsexp  12470  prmfac1  12474  eulerthlemrprm  12551  eulerthlema  12552  reumodprminv  12576  pcmpt  12666  pcfac  12673  prmpwdvds  12678  ennnfoneleminc  12782  ennnfonelemkh  12783  ennnfonelemhf1o  12784  ennnfonelemhom  12786  nninfdclemlt  12822  gsumfzz  13327  mulgnnass  13493  mhmmulg  13499  gsumfzconst  13677  srgmulgass  13751  srgpcomp  13752  lmodvsmmulgdi  14085  cnfldexp  14339  gsumfzfsumlemm  14349  mplelbascoe  14454  fiinopn  14476  cnpfval  14667  iscnp3  14675  cnprcl2k  14678  tgcn  14680  lmbr  14685  lmbr2  14686  lmbrf  14687  lmss  14718  cnmptcom  14770  metss  14966  metcnp  14984  metcnpi  14987  metcnpi2  14988  elcncf  15045  cncfi  15050  rescncf  15053  cncfco  15063  cdivcncfap  15076  ellimc3apf  15132  limcdifap  15134  limcmpted  15135  limcimo  15137  limcresi  15138  cnplimclemr  15141  limccoap  15150  dvmptfsum  15197  plycolemc  15230  rpcxpmul2  15385  perfectlem2  15472  lgsquad2lem2  15559  bdbm1.3ii  15827  bj-2inf  15874  bj-omtrans  15892  nninfalllem1  15945  nninfsellemdc  15947  nninfsellemqall  15952