Theorem imbi2d 230

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

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  imbi12d  234  imbi2  237  pm5.42  320  imanst  893  pm4.14dc  895  imimorbdc  901  pm5.6dc  931  ax11v2  1866  ax11v  1873  equs5or  1876  mo23  2119  nfabdw  2391  2gencl  2834  3gencl  2835  vtocl2gf  2864  vtocl3gf  2865  vtocl4g  2873  vtocl4ga  2874  eqeu  2974  mo2icl  2983  euind  2991  reu7  2999  reuind  3009  sbctt  3096  reu8nf  3111  sbcnestgf  3177  preq12bg  3854  elint  3932  elintrabg  3939  intab  3955  trss  4194  bm1.3ii  4208  pocl  4398  swopolem  4400  sowlin  4415  frforeq3  4442  frirrg  4445  frind  4447  reusv3  4555  regexmid  4631  ordsoexmid  4658  tfisi  4683  finds2  4697  nnregexmid  4717  vtoclr  4772  2optocl  4801  3optocl  4802  raliunxp  4869  resieq  5021  iss  5057  cnveqb  5190  iotaexab  5303  funmo  5339  fnbrfvb  5680  fvelimab  5698  fvmptssdm  5727  fmptco  5809  fnressn  5835  fressnfv  5836  isoselem  5956  isosolem  5960  ovg  6156  caovcan  6182  caovordig  6183  caovord  6189  f1o2ndf1  6388  poxp  6392  smoeq  6451  smores  6453  tfrlem1  6469  tfrlemi1  6493  tfrexlem  6495  tfri3  6528  oawordriexmid  6633  nnacl  6643  nnmcl  6644  nnacom  6647  nnaass  6648  nndi  6649  nnmass  6650  nnmsucr  6651  nnmcom  6652  nnsucsssuc  6655  nntri3or  6656  nnaordi  6671  nnaword  6674  nnmordi  6679  nnaordex  6691  2ecoptocl  6787  3ecoptocl  6788  th3qlem2  6802  xpdom2g  7011  findcard2  7071  findcard2s  7072  xpfi  7117  supeq1  7176  ordiso2  7225  updjud  7272  nnnninfeq  7318  exmidontriimlem4  7429  exmidontriim  7430  distrnq0  7669  addassnq0  7672  elinp  7684  prcdnql  7694  prcunqu  7695  prarloclem3  7707  caucvgpr  7892  caucvgprpr  7922  ltsosr  7974  caucvgsrlemcau  8003  caucvgsrlemgt1  8005  caucvgsrlemoffres  8010  pitonn  8058  axpre-ltwlin  8093  axcaucvglemres  8109  sup3exmid  9127  nnaddcl  9153  nnmulcl  9154  zaddcllempos  9506  zaddcllemneg  9508  prime  9569  peano5uzti  9578  uzind2  9582  zindd  9588  uzaddcl  9810  exfzdc  10476  infssuzex  10483  nninfdcex  10487  frec2uzltd  10655  frec2uzrdg  10661  frecuzrdgtcl  10664  frecuzrdgg  10668  frecuzrdgfunlem  10671  seq3val  10712  seqvalcd  10713  seq3clss  10723  seq3fveq2  10727  seqfveq2g  10729  seq3shft2  10733  seqshft2g  10734  monoord  10737  seq3split  10740  seqsplitg  10741  seq3caopr3  10743  seqcaopr3g  10744  seq3f1olemp  10767  seqf1oglem2a  10770  seqf1og  10773  seq3id3  10776  seq3id2  10778  seq3homo  10779  seq3z  10780  seqhomog  10782  seqfeq4g  10783  ser3ge0  10788  exp3vallem  10792  expcllem  10802  expap0  10821  mulexp  10830  expadd  10833  expmul  10836  leexp2r  10845  leexp1a  10846  bernneq  10912  modqexp  10918  nn0ltexp2  10961  apexp1  10970  facdiv  10990  faclbnd  10993  faclbnd6  10996  omgadd  11055  seq3coll  11096  wrdind  11293  wrd2ind  11294  pfxccatin12lem3  11303  shftvalg  11387  shftval4g  11388  cjexp  11444  resqrexlemover  11561  resqrexlemdecn  11563  resqrexlemlo  11564  resqrexlemcalc3  11567  absexp  11630  climshft  11855  climub  11895  climserle  11896  fsum2d  11986  fsumabs  12016  fsumiun  12028  binom  12035  bcxmas  12040  cvgratnnlemnexp  12075  cvgratnnlemmn  12076  clim2prod  12090  prodfap0  12096  prodfrecap  12097  fprodabs  12167  fprod2d  12174  demoivreALT  12325  dvdsfac  12411  bitsinv1  12513  bezoutlemstep  12558  bezoutlemmain  12559  bezoutlemex  12562  dfgcd2  12575  gcdmultiple  12581  rplpwr  12588  nn0seqcvgd  12603  alginv  12609  algcvga  12613  algfx  12614  isprm4  12681  prmind2  12682  prmdvdsexp  12710  prmfac1  12714  eulerthlemrprm  12791  eulerthlema  12792  reumodprminv  12816  pcmpt  12906  pcfac  12913  prmpwdvds  12918  ennnfoneleminc  13022  ennnfonelemkh  13023  ennnfonelemhf1o  13024  ennnfonelemhom  13026  nninfdclemlt  13062  gsumfzz  13568  mulgnnass  13734  mhmmulg  13740  gsumfzconst  13918  srgmulgass  13992  srgpcomp  13993  lmodvsmmulgdi  14327  cnfldexp  14581  gsumfzfsumlemm  14591  mplelbascoe  14696  fiinopn  14718  cnpfval  14909  iscnp3  14917  cnprcl2k  14920  tgcn  14922  lmbr  14927  lmbr2  14928  lmbrf  14929  lmss  14960  cnmptcom  15012  metss  15208  metcnp  15226  metcnpi  15229  metcnpi2  15230  elcncf  15287  cncfi  15292  rescncf  15295  cncfco  15305  cdivcncfap  15318  ellimc3apf  15374  limcdifap  15376  limcmpted  15377  limcimo  15379  limcresi  15380  cnplimclemr  15383  limccoap  15392  dvmptfsum  15439  plycolemc  15472  rpcxpmul2  15627  perfectlem2  15714  lgsquad2lem2  15801  bdbm1.3ii  16422  bj-2inf  16469  bj-omtrans  16487  nninfalllem1  16546  nninfsellemdc  16548  nninfsellemqall  16553