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-1 5  ax-2 6  ax-mp 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  316  imanst  854  pm4.14dc  856  imimorbdc  862  pm5.6dc  892  ax11v2  1772  ax11v  1779  equs5or  1782  mo23  2014  2gencl  2688  3gencl  2689  vtocl2gf  2717  vtocl3gf  2718  eqeu  2821  mo2icl  2830  euind  2838  reu7  2846  reuind  2856  sbctt  2941  sbcnestgf  3015  preq12bg  3664  elint  3741  elintrabg  3748  intab  3764  trss  3993  bm1.3ii  4007  pocl  4183  swopolem  4185  sowlin  4200  frforeq3  4227  frirrg  4230  frind  4232  reusv3  4339  regexmid  4408  ordsoexmid  4435  tfisi  4459  finds2  4473  nnregexmid  4492  vtoclr  4545  2optocl  4574  3optocl  4575  raliunxp  4638  resieq  4785  iss  4821  cnveqb  4950  funmo  5094  fnbrfvb  5414  fvelimab  5429  fvmptssdm  5457  fmptco  5538  fnressn  5558  fressnfv  5559  isoselem  5673  isosolem  5677  ovg  5861  caovcan  5887  caovordig  5888  caovord  5894  f1o2ndf1  6076  poxp  6080  smoeq  6138  smores  6140  tfrlem1  6156  tfrlemi1  6180  tfrexlem  6182  tfri3  6215  oawordriexmid  6317  nnacl  6327  nnmcl  6328  nnacom  6331  nnaass  6332  nndi  6333  nnmass  6334  nnmsucr  6335  nnmcom  6336  nnsucsssuc  6339  nntri3or  6340  nnaordi  6355  nnaword  6358  nnmordi  6363  nnaordex  6374  2ecoptocl  6468  3ecoptocl  6469  th3qlem2  6483  xpdom2g  6676  findcard2  6733  findcard2s  6734  xpfi  6768  supeq1  6822  ordiso2  6869  updjud  6916  distrnq0  7208  addassnq0  7211  elinp  7223  prcdnql  7233  prcunqu  7234  prarloclem3  7246  caucvgpr  7431  caucvgprpr  7461  ltsosr  7500  caucvgsrlemcau  7528  caucvgsrlemgt1  7530  caucvgsrlemoffres  7535  pitonn  7576  axpre-ltwlin  7611  axcaucvglemres  7627  sup3exmid  8618  nnaddcl  8643  nnmulcl  8644  zaddcllempos  8988  zaddcllemneg  8990  prime  9047  peano5uzti  9056  uzind2  9060  zindd  9066  uzaddcl  9276  exfzdc  9903  frec2uzltd  10062  frec2uzrdg  10068  frecuzrdgtcl  10071  frecuzrdgg  10075  frecuzrdgfunlem  10078  seq3val  10117  seqvalcd  10118  seq3clss  10126  seq3fveq2  10128  seq3shft2  10132  monoord  10135  seq3split  10138  seq3caopr3  10140  seq3f1olemp  10161  seq3id3  10166  seq3id2  10168  seq3homo  10169  seq3z  10170  ser3ge0  10176  exp3vallem  10180  expcllem  10190  expap0  10209  mulexp  10218  expadd  10221  expmul  10224  leexp2r  10233  leexp1a  10234  bernneq  10298  facdiv  10370  faclbnd  10373  faclbnd6  10376  omgadd  10434  seq3coll  10471  shftvalg  10494  shftval4g  10495  cjexp  10551  resqrexlemover  10667  resqrexlemdecn  10669  resqrexlemlo  10670  resqrexlemcalc3  10673  absexp  10736  climshft  10958  climub  10998  climserle  10999  fsum2d  11089  fsumabs  11119  fsumiun  11131  binom  11138  bcxmas  11143  cvgratnnlemnexp  11178  cvgratnnlemmn  11179  demoivreALT  11323  dvdsfac  11399  infssuzex  11483  bezoutlemstep  11524  bezoutlemmain  11525  bezoutlemex  11528  dfgcd2  11541  gcdmultiple  11547  rplpwr  11554  nn0seqcvgd  11561  alginv  11567  algcvga  11571  algfx  11572  isprm4  11639  prmind2  11640  prmdvdsexp  11665  prmfac1  11669  ennnfoneleminc  11762  ennnfonelemkh  11763  ennnfonelemhf1o  11764  ennnfonelemhom  11766  fiinopn  12007  cnpfval  12200  iscnp3  12207  cnprcl2k  12210  tgcn  12212  lmbr  12217  lmbr2  12218  lmbrf  12219  lmss  12250  cnmptcom  12302  metss  12476  metcnp  12494  metcnpi  12497  metcnpi2  12498  elcncf  12539  cncfi  12544  rescncf  12547  cncfco  12557  cdivcncfap  12566  ellimc3apf  12578  limcdifap  12580  limcmpted  12581  limcimo  12583  limcresi  12584  cnplimclemr  12587  bdbm1.3ii  12768  bj-2inf  12815  bj-omtrans  12833  nninfalllemn  12879  nninfalllem1  12880  nninfsellemdc  12883  nninfsellemqall  12888