Theorem imbi2d 219

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 171	1 |- ( ph -> ( ( th -> ps ) <-> ( th -> ch ) ) )

Syntax hints:   -> wi 4   <-> wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  imbi12d  223  imbi2  226  pm5.42  303  imandc  786  pm4.14dc  787  imimorbdc  795  pm5.6dc  835  ax11v2  1701  ax11v  1708  equs5or  1711  mo23  1941  2gencl  2587  3gencl  2588  vtocl2gf  2615  vtocl3gf  2616  eqeu  2711  mo2icl  2720  euind  2728  reu7  2736  reuind  2744  sbctt  2824  sbcnestgf  2897  preq12bg  3544  elint  3621  elintrabg  3628  intab  3644  trss  3863  bm1.3ii  3878  pocl  4040  swopolem  4042  sowlin  4057  frforeq3  4084  frirrg  4087  frind  4089  reusv3  4192  regexmid  4260  ordsoexmid  4286  tfisi  4310  finds2  4324  nnregexmid  4342  vtoclr  4388  2optocl  4417  3optocl  4418  raliunxp  4477  resieq  4622  iss  4654  cnveqb  4776  funmo  4917  fnbrfvb  5214  fvelimab  5229  fvmptssdm  5255  fmptco  5330  fnressn  5349  fressnfv  5350  isoselem  5459  isosolem  5463  ovg  5639  caovcan  5665  caovordig  5666  caovord  5672  f1o2ndf1  5849  poxp  5853  smoeq  5905  smores  5907  tfrlem1  5923  tfrlemi1  5946  tfrexlem  5948  tfri3  5953  rdgon  5973  freccl  5993  nnacl  6059  nnmcl  6060  nnacom  6063  nnaass  6064  nndi  6065  nnmass  6066  nnmsucr  6067  nnmcom  6068  nnsucsssuc  6071  nntri3or  6072  nnaordi  6081  nnaword  6084  nnmordi  6089  nnaordex  6100  2ecoptocl  6194  3ecoptocl  6195  th3qlem2  6209  xpdom2g  6306  findcard2  6346  findcard2s  6347  ordiso2  6357  distrnq0  6557  addassnq0  6560  elinp  6572  prcdnql  6582  prcunqu  6583  prarloclem3  6595  caucvgpr  6780  caucvgprpr  6810  ltsosr  6849  caucvgsrlemcau  6877  caucvgsrlemgt1  6879  caucvgsrlemoffres  6884  pitonn  6924  axpre-ltwlin  6957  axcaucvglemres  6973  nnaddcl  7934  nnmulcl  7935  zaddcllempos  8282  zaddcllemneg  8284  prime  8337  peano5uzti  8346  uzind2  8350  zindd  8356  uzaddcl  8529  frec2uzltd  9189  frec2uzrdg  9195  frecuzrdgfn  9198  iseqss  9226  iseqfveq2  9228  iseqshft2  9232  monoord  9235  iseqsplit  9238  iseqcaopr3  9240  iseqid3s  9246  iseqhomo  9248  expivallem  9256  expcllem  9266  expap0  9285  mulexp  9294  expadd  9297  expmul  9300  leexp2r  9308  leexp1a  9309  bernneq  9369  shftvalg  9437  shftval4g  9438  cjexp  9493  resqrexlemover  9608  resqrexlemdecn  9610  resqrexlemlo  9611  resqrexlemcalc3  9614  absexp  9675  climshft  9825  climub  9864  climserile  9865  nn0seqcvgd  9880  ialginv  9886  ialgcvga  9890  ialgfx  9891  bdbm1.3ii  10011  bj-2inf  10062  bj-omtrans  10081