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  878  pm4.14dc  880  imimorbdc  886  pm5.6dc  916  ax11v2  1808  ax11v  1815  equs5or  1818  mo23  2055  nfabdw  2326  2gencl  2758  3gencl  2759  vtocl2gf  2787  vtocl3gf  2788  eqeu  2895  mo2icl  2904  euind  2912  reu7  2920  reuind  2930  sbctt  3016  sbcnestgf  3095  preq12bg  3752  elint  3829  elintrabg  3836  intab  3852  trss  4088  bm1.3ii  4102  pocl  4280  swopolem  4282  sowlin  4297  frforeq3  4324  frirrg  4327  frind  4329  reusv3  4437  regexmid  4511  ordsoexmid  4538  tfisi  4563  finds2  4577  nnregexmid  4597  vtoclr  4651  2optocl  4680  3optocl  4681  raliunxp  4744  resieq  4893  iss  4929  cnveqb  5058  funmo  5202  fnbrfvb  5526  fvelimab  5541  fvmptssdm  5569  fmptco  5650  fnressn  5670  fressnfv  5671  isoselem  5787  isosolem  5791  ovg  5976  caovcan  6002  caovordig  6003  caovord  6009  f1o2ndf1  6192  poxp  6196  smoeq  6254  smores  6256  tfrlem1  6272  tfrlemi1  6296  tfrexlem  6298  tfri3  6331  oawordriexmid  6434  nnacl  6444  nnmcl  6445  nnacom  6448  nnaass  6449  nndi  6450  nnmass  6451  nnmsucr  6452  nnmcom  6453  nnsucsssuc  6456  nntri3or  6457  nnaordi  6472  nnaword  6475  nnmordi  6480  nnaordex  6491  2ecoptocl  6585  3ecoptocl  6586  th3qlem2  6600  xpdom2g  6794  findcard2  6851  findcard2s  6852  xpfi  6891  supeq1  6947  ordiso2  6996  updjud  7043  nnnninfeq  7088  exmidontriimlem4  7176  exmidontriim  7177  distrnq0  7396  addassnq0  7399  elinp  7411  prcdnql  7421  prcunqu  7422  prarloclem3  7434  caucvgpr  7619  caucvgprpr  7649  ltsosr  7701  caucvgsrlemcau  7730  caucvgsrlemgt1  7732  caucvgsrlemoffres  7737  pitonn  7785  axpre-ltwlin  7820  axcaucvglemres  7836  sup3exmid  8848  nnaddcl  8873  nnmulcl  8874  zaddcllempos  9224  zaddcllemneg  9226  prime  9286  peano5uzti  9295  uzind2  9299  zindd  9305  uzaddcl  9520  exfzdc  10171  frec2uzltd  10334  frec2uzrdg  10340  frecuzrdgtcl  10343  frecuzrdgg  10347  frecuzrdgfunlem  10350  seq3val  10389  seqvalcd  10390  seq3clss  10398  seq3fveq2  10400  seq3shft2  10404  monoord  10407  seq3split  10410  seq3caopr3  10412  seq3f1olemp  10433  seq3id3  10438  seq3id2  10440  seq3homo  10441  seq3z  10442  ser3ge0  10448  exp3vallem  10452  expcllem  10462  expap0  10481  mulexp  10490  expadd  10493  expmul  10496  leexp2r  10505  leexp1a  10506  bernneq  10571  modqexp  10577  nn0ltexp2  10619  apexp1  10627  facdiv  10647  faclbnd  10650  faclbnd6  10653  omgadd  10711  seq3coll  10751  shftvalg  10774  shftval4g  10775  cjexp  10831  resqrexlemover  10948  resqrexlemdecn  10950  resqrexlemlo  10951  resqrexlemcalc3  10954  absexp  11017  climshft  11241  climub  11281  climserle  11282  fsum2d  11372  fsumabs  11402  fsumiun  11414  binom  11421  bcxmas  11426  cvgratnnlemnexp  11461  cvgratnnlemmn  11462  clim2prod  11476  prodfap0  11482  prodfrecap  11483  fprodabs  11553  fprod2d  11560  demoivreALT  11710  dvdsfac  11794  infssuzex  11878  nninfdcex  11882  bezoutlemstep  11926  bezoutlemmain  11927  bezoutlemex  11930  dfgcd2  11943  gcdmultiple  11949  rplpwr  11956  nn0seqcvgd  11969  alginv  11975  algcvga  11979  algfx  11980  isprm4  12047  prmind2  12048  prmdvdsexp  12076  prmfac1  12080  eulerthlemrprm  12157  eulerthlema  12158  reumodprminv  12181  pcmpt  12269  pcfac  12276  prmpwdvds  12281  ennnfoneleminc  12340  ennnfonelemkh  12341  ennnfonelemhf1o  12342  ennnfonelemhom  12344  nninfdclemlt  12380  fiinopn  12602  cnpfval  12795  iscnp3  12803  cnprcl2k  12806  tgcn  12808  lmbr  12813  lmbr2  12814  lmbrf  12815  lmss  12846  cnmptcom  12898  metss  13094  metcnp  13112  metcnpi  13115  metcnpi2  13116  elcncf  13160  cncfi  13165  rescncf  13168  cncfco  13178  cdivcncfap  13187  ellimc3apf  13229  limcdifap  13231  limcmpted  13232  limcimo  13234  limcresi  13235  cnplimclemr  13238  limccoap  13247  bdbm1.3ii  13733  bj-2inf  13780  bj-omtrans  13798  nninfalllem1  13848  nninfsellemdc  13850  nninfsellemqall  13855