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  895  pm4.14dc  897  imimorbdc  903  pm5.6dc  933  ax11v2  1868  ax11v  1875  equs5or  1878  mo23  2121  nfabdw  2393  2gencl  2836  3gencl  2837  vtocl2gf  2866  vtocl3gf  2867  vtocl4g  2875  vtocl4ga  2876  eqeu  2976  mo2icl  2985  euind  2993  reu7  3001  reuind  3011  sbctt  3098  reu8nf  3113  sbcnestgf  3179  preq12bg  3856  elint  3934  elintrabg  3941  intab  3957  trss  4196  bm1.3ii  4210  pocl  4400  swopolem  4402  sowlin  4417  frforeq3  4444  frirrg  4447  frind  4449  reusv3  4557  regexmid  4633  ordsoexmid  4660  tfisi  4685  finds2  4699  nnregexmid  4719  vtoclr  4774  2optocl  4803  3optocl  4804  raliunxp  4871  resieq  5023  iss  5059  cnveqb  5192  iotaexab  5305  funmo  5341  fnbrfvb  5684  fvelimab  5702  fvmptssdm  5731  fmptco  5813  fnressn  5839  fressnfv  5840  isoselem  5960  isosolem  5964  ovg  6160  caovcan  6186  caovordig  6187  caovord  6193  f1o2ndf1  6392  poxp  6396  smoeq  6455  smores  6457  tfrlem1  6473  tfrlemi1  6497  tfrexlem  6499  tfri3  6532  oawordriexmid  6637  nnacl  6647  nnmcl  6648  nnacom  6651  nnaass  6652  nndi  6653  nnmass  6654  nnmsucr  6655  nnmcom  6656  nnsucsssuc  6659  nntri3or  6660  nnaordi  6675  nnaword  6678  nnmordi  6683  nnaordex  6695  2ecoptocl  6791  3ecoptocl  6792  th3qlem2  6806  xpdom2g  7015  findcard2  7077  findcard2s  7078  xpfi  7123  supeq1  7184  ordiso2  7233  updjud  7280  nnnninfeq  7326  exmidontriimlem4  7438  exmidontriim  7439  distrnq0  7678  addassnq0  7681  elinp  7693  prcdnql  7703  prcunqu  7704  prarloclem3  7716  caucvgpr  7901  caucvgprpr  7931  ltsosr  7983  caucvgsrlemcau  8012  caucvgsrlemgt1  8014  caucvgsrlemoffres  8019  pitonn  8067  axpre-ltwlin  8102  axcaucvglemres  8118  sup3exmid  9136  nnaddcl  9162  nnmulcl  9163  zaddcllempos  9515  zaddcllemneg  9517  prime  9578  peano5uzti  9587  uzind2  9591  zindd  9597  uzaddcl  9819  exfzdc  10485  infssuzex  10492  nninfdcex  10496  frec2uzltd  10664  frec2uzrdg  10670  frecuzrdgtcl  10673  frecuzrdgg  10677  frecuzrdgfunlem  10680  seq3val  10721  seqvalcd  10722  seq3clss  10732  seq3fveq2  10736  seqfveq2g  10738  seq3shft2  10742  seqshft2g  10743  monoord  10746  seq3split  10749  seqsplitg  10750  seq3caopr3  10752  seqcaopr3g  10753  seq3f1olemp  10776  seqf1oglem2a  10779  seqf1og  10782  seq3id3  10785  seq3id2  10787  seq3homo  10788  seq3z  10789  seqhomog  10791  seqfeq4g  10792  ser3ge0  10797  exp3vallem  10801  expcllem  10811  expap0  10830  mulexp  10839  expadd  10842  expmul  10845  leexp2r  10854  leexp1a  10855  bernneq  10921  modqexp  10927  nn0ltexp2  10970  apexp1  10979  facdiv  10999  faclbnd  11002  faclbnd6  11005  omgadd  11064  seq3coll  11105  wrdind  11302  wrd2ind  11303  pfxccatin12lem3  11312  shftvalg  11396  shftval4g  11397  cjexp  11453  resqrexlemover  11570  resqrexlemdecn  11572  resqrexlemlo  11573  resqrexlemcalc3  11576  absexp  11639  climshft  11864  climub  11904  climserle  11905  fsum2d  11995  fsumabs  12025  fsumiun  12037  binom  12044  bcxmas  12049  cvgratnnlemnexp  12084  cvgratnnlemmn  12085  clim2prod  12099  prodfap0  12105  prodfrecap  12106  fprodabs  12176  fprod2d  12183  demoivreALT  12334  dvdsfac  12420  bitsinv1  12522  bezoutlemstep  12567  bezoutlemmain  12568  bezoutlemex  12571  dfgcd2  12584  gcdmultiple  12590  rplpwr  12597  nn0seqcvgd  12612  alginv  12618  algcvga  12622  algfx  12623  isprm4  12690  prmind2  12691  prmdvdsexp  12719  prmfac1  12723  eulerthlemrprm  12800  eulerthlema  12801  reumodprminv  12825  pcmpt  12915  pcfac  12922  prmpwdvds  12927  ennnfoneleminc  13031  ennnfonelemkh  13032  ennnfonelemhf1o  13033  ennnfonelemhom  13035  nninfdclemlt  13071  gsumfzz  13577  mulgnnass  13743  mhmmulg  13749  gsumfzconst  13927  srgmulgass  14001  srgpcomp  14002  lmodvsmmulgdi  14336  cnfldexp  14590  gsumfzfsumlemm  14600  mplelbascoe  14705  fiinopn  14727  cnpfval  14918  iscnp3  14926  cnprcl2k  14929  tgcn  14931  lmbr  14936  lmbr2  14937  lmbrf  14938  lmss  14969  cnmptcom  15021  metss  15217  metcnp  15235  metcnpi  15238  metcnpi2  15239  elcncf  15296  cncfi  15301  rescncf  15304  cncfco  15314  cdivcncfap  15327  ellimc3apf  15383  limcdifap  15385  limcmpted  15386  limcimo  15388  limcresi  15389  cnplimclemr  15392  limccoap  15401  dvmptfsum  15448  plycolemc  15481  rpcxpmul2  15636  perfectlem2  15723  lgsquad2lem2  15810  bdbm1.3ii  16486  bj-2inf  16533  bj-omtrans  16551  nninfalllem1  16610  nninfsellemdc  16612  nninfsellemqall  16617