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  5840  fressnfv  5841  isoselem  5961  isosolem  5965  ovg  6161  caovcan  6187  caovordig  6188  caovord  6194  f1o2ndf1  6393  poxp  6397  smoeq  6456  smores  6458  tfrlem1  6474  tfrlemi1  6498  tfrexlem  6500  tfri3  6533  oawordriexmid  6638  nnacl  6648  nnmcl  6649  nnacom  6652  nnaass  6653  nndi  6654  nnmass  6655  nnmsucr  6656  nnmcom  6657  nnsucsssuc  6660  nntri3or  6661  nnaordi  6676  nnaword  6679  nnmordi  6684  nnaordex  6696  2ecoptocl  6792  3ecoptocl  6793  th3qlem2  6807  xpdom2g  7016  findcard2  7078  findcard2s  7079  xpfi  7124  supeq1  7185  ordiso2  7234  updjud  7281  nnnninfeq  7327  exmidontriimlem4  7439  exmidontriim  7440  distrnq0  7679  addassnq0  7682  elinp  7694  prcdnql  7704  prcunqu  7705  prarloclem3  7717  caucvgpr  7902  caucvgprpr  7932  ltsosr  7984  caucvgsrlemcau  8013  caucvgsrlemgt1  8015  caucvgsrlemoffres  8020  pitonn  8068  axpre-ltwlin  8103  axcaucvglemres  8119  sup3exmid  9137  nnaddcl  9163  nnmulcl  9164  zaddcllempos  9516  zaddcllemneg  9518  prime  9579  peano5uzti  9588  uzind2  9592  zindd  9598  uzaddcl  9820  exfzdc  10487  infssuzex  10494  nninfdcex  10498  frec2uzltd  10666  frec2uzrdg  10672  frecuzrdgtcl  10675  frecuzrdgg  10679  frecuzrdgfunlem  10682  seq3val  10723  seqvalcd  10724  seq3clss  10734  seq3fveq2  10738  seqfveq2g  10740  seq3shft2  10744  seqshft2g  10745  monoord  10748  seq3split  10751  seqsplitg  10752  seq3caopr3  10754  seqcaopr3g  10755  seq3f1olemp  10778  seqf1oglem2a  10781  seqf1og  10784  seq3id3  10787  seq3id2  10789  seq3homo  10790  seq3z  10791  seqhomog  10793  seqfeq4g  10794  ser3ge0  10799  exp3vallem  10803  expcllem  10813  expap0  10832  mulexp  10841  expadd  10844  expmul  10847  leexp2r  10856  leexp1a  10857  bernneq  10923  modqexp  10929  nn0ltexp2  10972  apexp1  10981  facdiv  11001  faclbnd  11004  faclbnd6  11007  omgadd  11066  seq3coll  11107  wrdind  11307  wrd2ind  11308  pfxccatin12lem3  11317  shftvalg  11414  shftval4g  11415  cjexp  11471  resqrexlemover  11588  resqrexlemdecn  11590  resqrexlemlo  11591  resqrexlemcalc3  11594  absexp  11657  climshft  11882  climub  11922  climserle  11923  fsum2d  12014  fsumabs  12044  fsumiun  12056  binom  12063  bcxmas  12068  cvgratnnlemnexp  12103  cvgratnnlemmn  12104  clim2prod  12118  prodfap0  12124  prodfrecap  12125  fprodabs  12195  fprod2d  12202  demoivreALT  12353  dvdsfac  12439  bitsinv1  12541  bezoutlemstep  12586  bezoutlemmain  12587  bezoutlemex  12590  dfgcd2  12603  gcdmultiple  12609  rplpwr  12616  nn0seqcvgd  12631  alginv  12637  algcvga  12641  algfx  12642  isprm4  12709  prmind2  12710  prmdvdsexp  12738  prmfac1  12742  eulerthlemrprm  12819  eulerthlema  12820  reumodprminv  12844  pcmpt  12934  pcfac  12941  prmpwdvds  12946  ennnfoneleminc  13050  ennnfonelemkh  13051  ennnfonelemhf1o  13052  ennnfonelemhom  13054  nninfdclemlt  13090  gsumfzz  13596  mulgnnass  13762  mhmmulg  13768  gsumfzconst  13946  srgmulgass  14021  srgpcomp  14022  lmodvsmmulgdi  14356  cnfldexp  14610  gsumfzfsumlemm  14620  mplelbascoe  14725  fiinopn  14747  cnpfval  14938  iscnp3  14946  cnprcl2k  14949  tgcn  14951  lmbr  14956  lmbr2  14957  lmbrf  14958  lmss  14989  cnmptcom  15041  metss  15237  metcnp  15255  metcnpi  15258  metcnpi2  15259  elcncf  15316  cncfi  15321  rescncf  15324  cncfco  15334  cdivcncfap  15347  ellimc3apf  15403  limcdifap  15405  limcmpted  15406  limcimo  15408  limcresi  15409  cnplimclemr  15412  limccoap  15421  dvmptfsum  15468  plycolemc  15501  rpcxpmul2  15656  perfectlem2  15743  lgsquad2lem2  15830  eupth2fi  16349  depindlem2  16377  depindlem3  16378  bdbm1.3ii  16537  bj-2inf  16584  bj-omtrans  16602  nninfalllem1  16661  nninfsellemdc  16663  nninfsellemqall  16668