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  888  pm4.14dc  890  imimorbdc  896  pm5.6dc  926  ax11v2  1820  ax11v  1827  equs5or  1830  mo23  2067  nfabdw  2338  2gencl  2770  3gencl  2771  vtocl2gf  2799  vtocl3gf  2800  eqeu  2907  mo2icl  2916  euind  2924  reu7  2932  reuind  2942  sbctt  3029  sbcnestgf  3108  preq12bg  3773  elint  3850  elintrabg  3857  intab  3873  trss  4109  bm1.3ii  4123  pocl  4302  swopolem  4304  sowlin  4319  frforeq3  4346  frirrg  4349  frind  4351  reusv3  4459  regexmid  4533  ordsoexmid  4560  tfisi  4585  finds2  4599  nnregexmid  4619  vtoclr  4673  2optocl  4702  3optocl  4703  raliunxp  4767  resieq  4916  iss  4952  cnveqb  5083  funmo  5230  fnbrfvb  5555  fvelimab  5571  fvmptssdm  5599  fmptco  5681  fnressn  5701  fressnfv  5702  isoselem  5818  isosolem  5822  ovg  6010  caovcan  6036  caovordig  6037  caovord  6043  f1o2ndf1  6226  poxp  6230  smoeq  6288  smores  6290  tfrlem1  6306  tfrlemi1  6330  tfrexlem  6332  tfri3  6365  oawordriexmid  6468  nnacl  6478  nnmcl  6479  nnacom  6482  nnaass  6483  nndi  6484  nnmass  6485  nnmsucr  6486  nnmcom  6487  nnsucsssuc  6490  nntri3or  6491  nnaordi  6506  nnaword  6509  nnmordi  6514  nnaordex  6526  2ecoptocl  6620  3ecoptocl  6621  th3qlem2  6635  xpdom2g  6829  findcard2  6886  findcard2s  6887  xpfi  6926  supeq1  6982  ordiso2  7031  updjud  7078  nnnninfeq  7123  exmidontriimlem4  7220  exmidontriim  7221  distrnq0  7455  addassnq0  7458  elinp  7470  prcdnql  7480  prcunqu  7481  prarloclem3  7493  caucvgpr  7678  caucvgprpr  7708  ltsosr  7760  caucvgsrlemcau  7789  caucvgsrlemgt1  7791  caucvgsrlemoffres  7796  pitonn  7844  axpre-ltwlin  7879  axcaucvglemres  7895  sup3exmid  8910  nnaddcl  8935  nnmulcl  8936  zaddcllempos  9286  zaddcllemneg  9288  prime  9348  peano5uzti  9357  uzind2  9361  zindd  9367  uzaddcl  9582  exfzdc  10235  frec2uzltd  10398  frec2uzrdg  10404  frecuzrdgtcl  10407  frecuzrdgg  10411  frecuzrdgfunlem  10414  seq3val  10453  seqvalcd  10454  seq3clss  10462  seq3fveq2  10464  seq3shft2  10468  monoord  10471  seq3split  10474  seq3caopr3  10476  seq3f1olemp  10497  seq3id3  10502  seq3id2  10504  seq3homo  10505  seq3z  10506  ser3ge0  10512  exp3vallem  10516  expcllem  10526  expap0  10545  mulexp  10554  expadd  10557  expmul  10560  leexp2r  10569  leexp1a  10570  bernneq  10635  modqexp  10641  nn0ltexp2  10683  apexp1  10691  facdiv  10711  faclbnd  10714  faclbnd6  10717  omgadd  10775  seq3coll  10815  shftvalg  10838  shftval4g  10839  cjexp  10895  resqrexlemover  11012  resqrexlemdecn  11014  resqrexlemlo  11015  resqrexlemcalc3  11018  absexp  11081  climshft  11305  climub  11345  climserle  11346  fsum2d  11436  fsumabs  11466  fsumiun  11478  binom  11485  bcxmas  11490  cvgratnnlemnexp  11525  cvgratnnlemmn  11526  clim2prod  11540  prodfap0  11546  prodfrecap  11547  fprodabs  11617  fprod2d  11624  demoivreALT  11774  dvdsfac  11858  infssuzex  11942  nninfdcex  11946  bezoutlemstep  11990  bezoutlemmain  11991  bezoutlemex  11994  dfgcd2  12007  gcdmultiple  12013  rplpwr  12020  nn0seqcvgd  12033  alginv  12039  algcvga  12043  algfx  12044  isprm4  12111  prmind2  12112  prmdvdsexp  12140  prmfac1  12144  eulerthlemrprm  12221  eulerthlema  12222  reumodprminv  12245  pcmpt  12333  pcfac  12340  prmpwdvds  12345  ennnfoneleminc  12404  ennnfonelemkh  12405  ennnfonelemhf1o  12406  ennnfonelemhom  12408  nninfdclemlt  12444  mulgnnass  12949  mhmmulg  12955  srgmulgass  13103  srgpcomp  13104  cnfldexp  13340  fiinopn  13373  cnpfval  13566  iscnp3  13574  cnprcl2k  13577  tgcn  13579  lmbr  13584  lmbr2  13585  lmbrf  13586  lmss  13617  cnmptcom  13669  metss  13865  metcnp  13883  metcnpi  13886  metcnpi2  13887  elcncf  13931  cncfi  13936  rescncf  13939  cncfco  13949  cdivcncfap  13958  ellimc3apf  14000  limcdifap  14002  limcmpted  14003  limcimo  14005  limcresi  14006  cnplimclemr  14009  limccoap  14018  bdbm1.3ii  14503  bj-2inf  14550  bj-omtrans  14568  nninfalllem1  14617  nninfsellemdc  14619  nninfsellemqall  14624