Theorem imbi2d 229

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  imbi12d  233  imbi2  236  pm5.42  318  imanst  874  pm4.14dc  876  imimorbdc  882  pm5.6dc  912  ax11v2  1800  ax11v  1807  equs5or  1810  mo23  2047  nfabdw  2318  2gencl  2745  3gencl  2746  vtocl2gf  2774  vtocl3gf  2775  eqeu  2882  mo2icl  2891  euind  2899  reu7  2907  reuind  2917  sbctt  3003  sbcnestgf  3082  preq12bg  3736  elint  3813  elintrabg  3820  intab  3836  trss  4071  bm1.3ii  4085  pocl  4263  swopolem  4265  sowlin  4280  frforeq3  4307  frirrg  4310  frind  4312  reusv3  4420  regexmid  4494  ordsoexmid  4521  tfisi  4546  finds2  4560  nnregexmid  4580  vtoclr  4634  2optocl  4663  3optocl  4664  raliunxp  4727  resieq  4876  iss  4912  cnveqb  5041  funmo  5185  fnbrfvb  5509  fvelimab  5524  fvmptssdm  5552  fmptco  5633  fnressn  5653  fressnfv  5654  isoselem  5770  isosolem  5774  ovg  5959  caovcan  5985  caovordig  5986  caovord  5992  f1o2ndf1  6175  poxp  6179  smoeq  6237  smores  6239  tfrlem1  6255  tfrlemi1  6279  tfrexlem  6281  tfri3  6314  oawordriexmid  6417  nnacl  6427  nnmcl  6428  nnacom  6431  nnaass  6432  nndi  6433  nnmass  6434  nnmsucr  6435  nnmcom  6436  nnsucsssuc  6439  nntri3or  6440  nnaordi  6455  nnaword  6458  nnmordi  6463  nnaordex  6474  2ecoptocl  6568  3ecoptocl  6569  th3qlem2  6583  xpdom2g  6777  findcard2  6834  findcard2s  6835  xpfi  6874  supeq1  6930  ordiso2  6979  updjud  7026  nnnninfeq  7071  exmidontriimlem4  7159  exmidontriim  7160  distrnq0  7379  addassnq0  7382  elinp  7394  prcdnql  7404  prcunqu  7405  prarloclem3  7417  caucvgpr  7602  caucvgprpr  7632  ltsosr  7684  caucvgsrlemcau  7713  caucvgsrlemgt1  7715  caucvgsrlemoffres  7720  pitonn  7768  axpre-ltwlin  7803  axcaucvglemres  7819  sup3exmid  8828  nnaddcl  8853  nnmulcl  8854  zaddcllempos  9204  zaddcllemneg  9206  prime  9263  peano5uzti  9272  uzind2  9276  zindd  9282  uzaddcl  9497  exfzdc  10139  frec2uzltd  10302  frec2uzrdg  10308  frecuzrdgtcl  10311  frecuzrdgg  10315  frecuzrdgfunlem  10318  seq3val  10357  seqvalcd  10358  seq3clss  10366  seq3fveq2  10368  seq3shft2  10372  monoord  10375  seq3split  10378  seq3caopr3  10380  seq3f1olemp  10401  seq3id3  10406  seq3id2  10408  seq3homo  10409  seq3z  10410  ser3ge0  10416  exp3vallem  10420  expcllem  10430  expap0  10449  mulexp  10458  expadd  10461  expmul  10464  leexp2r  10473  leexp1a  10474  bernneq  10538  modqexp  10544  apexp1  10592  facdiv  10612  faclbnd  10615  faclbnd6  10618  omgadd  10676  seq3coll  10713  shftvalg  10736  shftval4g  10737  cjexp  10793  resqrexlemover  10910  resqrexlemdecn  10912  resqrexlemlo  10913  resqrexlemcalc3  10916  absexp  10979  climshft  11201  climub  11241  climserle  11242  fsum2d  11332  fsumabs  11362  fsumiun  11374  binom  11381  bcxmas  11386  cvgratnnlemnexp  11421  cvgratnnlemmn  11422  clim2prod  11436  prodfap0  11442  prodfrecap  11443  fprodabs  11513  fprod2d  11520  demoivreALT  11670  dvdsfac  11751  infssuzex  11835  nninfdcex  11838  bezoutlemstep  11880  bezoutlemmain  11881  bezoutlemex  11884  dfgcd2  11897  gcdmultiple  11903  rplpwr  11910  nn0seqcvgd  11917  alginv  11923  algcvga  11927  algfx  11928  isprm4  11995  prmind2  11996  prmdvdsexp  12022  prmfac1  12026  eulerthlemrprm  12103  eulerthlema  12104  ennnfoneleminc  12140  ennnfonelemkh  12141  ennnfonelemhf1o  12142  ennnfonelemhom  12144  nninfdclemlt  12182  fiinopn  12402  cnpfval  12595  iscnp3  12603  cnprcl2k  12606  tgcn  12608  lmbr  12613  lmbr2  12614  lmbrf  12615  lmss  12646  cnmptcom  12698  metss  12894  metcnp  12912  metcnpi  12915  metcnpi2  12916  elcncf  12960  cncfi  12965  rescncf  12968  cncfco  12978  cdivcncfap  12987  ellimc3apf  13029  limcdifap  13031  limcmpted  13032  limcimo  13034  limcresi  13035  cnplimclemr  13038  limccoap  13047  bdbm1.3ii  13466  bj-2inf  13513  bj-omtrans  13531  nninfalllem1  13580  nninfsellemdc  13582  nninfsellemqall  13587