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  873  pm4.14dc  875  imimorbdc  881  pm5.6dc  911  ax11v2  1792  ax11v  1799  equs5or  1802  mo23  2038  2gencl  2714  3gencl  2715  vtocl2gf  2743  vtocl3gf  2744  eqeu  2849  mo2icl  2858  euind  2866  reu7  2874  reuind  2884  sbctt  2970  sbcnestgf  3046  preq12bg  3695  elint  3772  elintrabg  3779  intab  3795  trss  4030  bm1.3ii  4044  pocl  4220  swopolem  4222  sowlin  4237  frforeq3  4264  frirrg  4267  frind  4269  reusv3  4376  regexmid  4445  ordsoexmid  4472  tfisi  4496  finds2  4510  nnregexmid  4529  vtoclr  4582  2optocl  4611  3optocl  4612  raliunxp  4675  resieq  4824  iss  4860  cnveqb  4989  funmo  5133  fnbrfvb  5455  fvelimab  5470  fvmptssdm  5498  fmptco  5579  fnressn  5599  fressnfv  5600  isoselem  5714  isosolem  5718  ovg  5902  caovcan  5928  caovordig  5929  caovord  5935  f1o2ndf1  6118  poxp  6122  smoeq  6180  smores  6182  tfrlem1  6198  tfrlemi1  6222  tfrexlem  6224  tfri3  6257  oawordriexmid  6359  nnacl  6369  nnmcl  6370  nnacom  6373  nnaass  6374  nndi  6375  nnmass  6376  nnmsucr  6377  nnmcom  6378  nnsucsssuc  6381  nntri3or  6382  nnaordi  6397  nnaword  6400  nnmordi  6405  nnaordex  6416  2ecoptocl  6510  3ecoptocl  6511  th3qlem2  6525  xpdom2g  6719  findcard2  6776  findcard2s  6777  xpfi  6811  supeq1  6866  ordiso2  6913  updjud  6960  distrnq0  7260  addassnq0  7263  elinp  7275  prcdnql  7285  prcunqu  7286  prarloclem3  7298  caucvgpr  7483  caucvgprpr  7513  ltsosr  7565  caucvgsrlemcau  7594  caucvgsrlemgt1  7596  caucvgsrlemoffres  7601  pitonn  7649  axpre-ltwlin  7684  axcaucvglemres  7700  sup3exmid  8708  nnaddcl  8733  nnmulcl  8734  zaddcllempos  9084  zaddcllemneg  9086  prime  9143  peano5uzti  9152  uzind2  9156  zindd  9162  uzaddcl  9374  exfzdc  10010  frec2uzltd  10169  frec2uzrdg  10175  frecuzrdgtcl  10178  frecuzrdgg  10182  frecuzrdgfunlem  10185  seq3val  10224  seqvalcd  10225  seq3clss  10233  seq3fveq2  10235  seq3shft2  10239  monoord  10242  seq3split  10245  seq3caopr3  10247  seq3f1olemp  10268  seq3id3  10273  seq3id2  10275  seq3homo  10276  seq3z  10277  ser3ge0  10283  exp3vallem  10287  expcllem  10297  expap0  10316  mulexp  10325  expadd  10328  expmul  10331  leexp2r  10340  leexp1a  10341  bernneq  10405  facdiv  10477  faclbnd  10480  faclbnd6  10483  omgadd  10541  seq3coll  10578  shftvalg  10601  shftval4g  10602  cjexp  10658  resqrexlemover  10775  resqrexlemdecn  10777  resqrexlemlo  10778  resqrexlemcalc3  10781  absexp  10844  climshft  11066  climub  11106  climserle  11107  fsum2d  11197  fsumabs  11227  fsumiun  11239  binom  11246  bcxmas  11251  cvgratnnlemnexp  11286  cvgratnnlemmn  11287  clim2prod  11301  prodfap0  11307  prodfrecap  11308  demoivreALT  11469  dvdsfac  11547  infssuzex  11631  bezoutlemstep  11674  bezoutlemmain  11675  bezoutlemex  11678  dfgcd2  11691  gcdmultiple  11697  rplpwr  11704  nn0seqcvgd  11711  alginv  11717  algcvga  11721  algfx  11722  isprm4  11789  prmind2  11790  prmdvdsexp  11815  prmfac1  11819  ennnfoneleminc  11913  ennnfonelemkh  11914  ennnfonelemhf1o  11915  ennnfonelemhom  11917  fiinopn  12160  cnpfval  12353  iscnp3  12361  cnprcl2k  12364  tgcn  12366  lmbr  12371  lmbr2  12372  lmbrf  12373  lmss  12404  cnmptcom  12456  metss  12652  metcnp  12670  metcnpi  12673  metcnpi2  12674  elcncf  12718  cncfi  12723  rescncf  12726  cncfco  12736  cdivcncfap  12745  ellimc3apf  12787  limcdifap  12789  limcmpted  12790  limcimo  12792  limcresi  12793  cnplimclemr  12796  limccoap  12805  bdbm1.3ii  13078  bj-2inf  13125  bj-omtrans  13143  nninfalllemn  13191  nninfalllem1  13192  nninfsellemdc  13195  nninfsellemqall  13200