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  890  pm4.14dc  892  imimorbdc  898  pm5.6dc  928  ax11v2  1844  ax11v  1851  equs5or  1854  mo23  2097  nfabdw  2369  2gencl  2810  3gencl  2811  vtocl2gf  2840  vtocl3gf  2841  vtocl4g  2849  vtocl4ga  2850  eqeu  2950  mo2icl  2959  euind  2967  reu7  2975  reuind  2985  sbctt  3072  reu8nf  3087  sbcnestgf  3153  preq12bg  3827  elint  3905  elintrabg  3912  intab  3928  trss  4167  bm1.3ii  4181  pocl  4368  swopolem  4370  sowlin  4385  frforeq3  4412  frirrg  4415  frind  4417  reusv3  4525  regexmid  4601  ordsoexmid  4628  tfisi  4653  finds2  4667  nnregexmid  4687  vtoclr  4741  2optocl  4770  3optocl  4771  raliunxp  4837  resieq  4988  iss  5024  cnveqb  5157  iotaexab  5269  funmo  5305  fnbrfvb  5642  fvelimab  5658  fvmptssdm  5687  fmptco  5769  fnressn  5793  fressnfv  5794  isoselem  5912  isosolem  5916  ovg  6108  caovcan  6134  caovordig  6135  caovord  6141  f1o2ndf1  6337  poxp  6341  smoeq  6399  smores  6401  tfrlem1  6417  tfrlemi1  6441  tfrexlem  6443  tfri3  6476  oawordriexmid  6579  nnacl  6589  nnmcl  6590  nnacom  6593  nnaass  6594  nndi  6595  nnmass  6596  nnmsucr  6597  nnmcom  6598  nnsucsssuc  6601  nntri3or  6602  nnaordi  6617  nnaword  6620  nnmordi  6625  nnaordex  6637  2ecoptocl  6733  3ecoptocl  6734  th3qlem2  6748  xpdom2g  6952  findcard2  7012  findcard2s  7013  xpfi  7055  supeq1  7114  ordiso2  7163  updjud  7210  nnnninfeq  7256  exmidontriimlem4  7367  exmidontriim  7368  distrnq0  7607  addassnq0  7610  elinp  7622  prcdnql  7632  prcunqu  7633  prarloclem3  7645  caucvgpr  7830  caucvgprpr  7860  ltsosr  7912  caucvgsrlemcau  7941  caucvgsrlemgt1  7943  caucvgsrlemoffres  7948  pitonn  7996  axpre-ltwlin  8031  axcaucvglemres  8047  sup3exmid  9065  nnaddcl  9091  nnmulcl  9092  zaddcllempos  9444  zaddcllemneg  9446  prime  9507  peano5uzti  9516  uzind2  9520  zindd  9526  uzaddcl  9742  exfzdc  10406  infssuzex  10413  nninfdcex  10417  frec2uzltd  10585  frec2uzrdg  10591  frecuzrdgtcl  10594  frecuzrdgg  10598  frecuzrdgfunlem  10601  seq3val  10642  seqvalcd  10643  seq3clss  10653  seq3fveq2  10657  seqfveq2g  10659  seq3shft2  10663  seqshft2g  10664  monoord  10667  seq3split  10670  seqsplitg  10671  seq3caopr3  10673  seqcaopr3g  10674  seq3f1olemp  10697  seqf1oglem2a  10700  seqf1og  10703  seq3id3  10706  seq3id2  10708  seq3homo  10709  seq3z  10710  seqhomog  10712  seqfeq4g  10713  ser3ge0  10718  exp3vallem  10722  expcllem  10732  expap0  10751  mulexp  10760  expadd  10763  expmul  10766  leexp2r  10775  leexp1a  10776  bernneq  10842  modqexp  10848  nn0ltexp2  10891  apexp1  10900  facdiv  10920  faclbnd  10923  faclbnd6  10926  omgadd  10984  seq3coll  11024  wrdind  11213  wrd2ind  11214  pfxccatin12lem3  11223  shftvalg  11262  shftval4g  11263  cjexp  11319  resqrexlemover  11436  resqrexlemdecn  11438  resqrexlemlo  11439  resqrexlemcalc3  11442  absexp  11505  climshft  11730  climub  11770  climserle  11771  fsum2d  11861  fsumabs  11891  fsumiun  11903  binom  11910  bcxmas  11915  cvgratnnlemnexp  11950  cvgratnnlemmn  11951  clim2prod  11965  prodfap0  11971  prodfrecap  11972  fprodabs  12042  fprod2d  12049  demoivreALT  12200  dvdsfac  12286  bitsinv1  12388  bezoutlemstep  12433  bezoutlemmain  12434  bezoutlemex  12437  dfgcd2  12450  gcdmultiple  12456  rplpwr  12463  nn0seqcvgd  12478  alginv  12484  algcvga  12488  algfx  12489  isprm4  12556  prmind2  12557  prmdvdsexp  12585  prmfac1  12589  eulerthlemrprm  12666  eulerthlema  12667  reumodprminv  12691  pcmpt  12781  pcfac  12788  prmpwdvds  12793  ennnfoneleminc  12897  ennnfonelemkh  12898  ennnfonelemhf1o  12899  ennnfonelemhom  12901  nninfdclemlt  12937  gsumfzz  13442  mulgnnass  13608  mhmmulg  13614  gsumfzconst  13792  srgmulgass  13866  srgpcomp  13867  lmodvsmmulgdi  14200  cnfldexp  14454  gsumfzfsumlemm  14464  mplelbascoe  14569  fiinopn  14591  cnpfval  14782  iscnp3  14790  cnprcl2k  14793  tgcn  14795  lmbr  14800  lmbr2  14801  lmbrf  14802  lmss  14833  cnmptcom  14885  metss  15081  metcnp  15099  metcnpi  15102  metcnpi2  15103  elcncf  15160  cncfi  15165  rescncf  15168  cncfco  15178  cdivcncfap  15191  ellimc3apf  15247  limcdifap  15249  limcmpted  15250  limcimo  15252  limcresi  15253  cnplimclemr  15256  limccoap  15265  dvmptfsum  15312  plycolemc  15345  rpcxpmul2  15500  perfectlem2  15587  lgsquad2lem2  15674  bdbm1.3ii  16026  bj-2inf  16073  bj-omtrans  16091  nninfalllem1  16147  nninfsellemdc  16149  nninfsellemqall  16154