Theorem imbi2d 229

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

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  imbi12d  233  imbi2  236  pm5.42  318  imanst  883  pm4.14dc  885  imimorbdc  891  pm5.6dc  921  ax11v2  1813  ax11v  1820  equs5or  1823  mo23  2060  nfabdw  2331  2gencl  2763  3gencl  2764  vtocl2gf  2792  vtocl3gf  2793  eqeu  2900  mo2icl  2909  euind  2917  reu7  2925  reuind  2935  sbctt  3021  sbcnestgf  3100  preq12bg  3760  elint  3837  elintrabg  3844  intab  3860  trss  4096  bm1.3ii  4110  pocl  4288  swopolem  4290  sowlin  4305  frforeq3  4332  frirrg  4335  frind  4337  reusv3  4445  regexmid  4519  ordsoexmid  4546  tfisi  4571  finds2  4585  nnregexmid  4605  vtoclr  4659  2optocl  4688  3optocl  4689  raliunxp  4752  resieq  4901  iss  4937  cnveqb  5066  funmo  5213  fnbrfvb  5537  fvelimab  5552  fvmptssdm  5580  fmptco  5662  fnressn  5682  fressnfv  5683  isoselem  5799  isosolem  5803  ovg  5991  caovcan  6017  caovordig  6018  caovord  6024  f1o2ndf1  6207  poxp  6211  smoeq  6269  smores  6271  tfrlem1  6287  tfrlemi1  6311  tfrexlem  6313  tfri3  6346  oawordriexmid  6449  nnacl  6459  nnmcl  6460  nnacom  6463  nnaass  6464  nndi  6465  nnmass  6466  nnmsucr  6467  nnmcom  6468  nnsucsssuc  6471  nntri3or  6472  nnaordi  6487  nnaword  6490  nnmordi  6495  nnaordex  6507  2ecoptocl  6601  3ecoptocl  6602  th3qlem2  6616  xpdom2g  6810  findcard2  6867  findcard2s  6868  xpfi  6907  supeq1  6963  ordiso2  7012  updjud  7059  nnnninfeq  7104  exmidontriimlem4  7201  exmidontriim  7202  distrnq0  7421  addassnq0  7424  elinp  7436  prcdnql  7446  prcunqu  7447  prarloclem3  7459  caucvgpr  7644  caucvgprpr  7674  ltsosr  7726  caucvgsrlemcau  7755  caucvgsrlemgt1  7757  caucvgsrlemoffres  7762  pitonn  7810  axpre-ltwlin  7845  axcaucvglemres  7861  sup3exmid  8873  nnaddcl  8898  nnmulcl  8899  zaddcllempos  9249  zaddcllemneg  9251  prime  9311  peano5uzti  9320  uzind2  9324  zindd  9330  uzaddcl  9545  exfzdc  10196  frec2uzltd  10359  frec2uzrdg  10365  frecuzrdgtcl  10368  frecuzrdgg  10372  frecuzrdgfunlem  10375  seq3val  10414  seqvalcd  10415  seq3clss  10423  seq3fveq2  10425  seq3shft2  10429  monoord  10432  seq3split  10435  seq3caopr3  10437  seq3f1olemp  10458  seq3id3  10463  seq3id2  10465  seq3homo  10466  seq3z  10467  ser3ge0  10473  exp3vallem  10477  expcllem  10487  expap0  10506  mulexp  10515  expadd  10518  expmul  10521  leexp2r  10530  leexp1a  10531  bernneq  10596  modqexp  10602  nn0ltexp2  10644  apexp1  10652  facdiv  10672  faclbnd  10675  faclbnd6  10678  omgadd  10737  seq3coll  10777  shftvalg  10800  shftval4g  10801  cjexp  10857  resqrexlemover  10974  resqrexlemdecn  10976  resqrexlemlo  10977  resqrexlemcalc3  10980  absexp  11043  climshft  11267  climub  11307  climserle  11308  fsum2d  11398  fsumabs  11428  fsumiun  11440  binom  11447  bcxmas  11452  cvgratnnlemnexp  11487  cvgratnnlemmn  11488  clim2prod  11502  prodfap0  11508  prodfrecap  11509  fprodabs  11579  fprod2d  11586  demoivreALT  11736  dvdsfac  11820  infssuzex  11904  nninfdcex  11908  bezoutlemstep  11952  bezoutlemmain  11953  bezoutlemex  11956  dfgcd2  11969  gcdmultiple  11975  rplpwr  11982  nn0seqcvgd  11995  alginv  12001  algcvga  12005  algfx  12006  isprm4  12073  prmind2  12074  prmdvdsexp  12102  prmfac1  12106  eulerthlemrprm  12183  eulerthlema  12184  reumodprminv  12207  pcmpt  12295  pcfac  12302  prmpwdvds  12307  ennnfoneleminc  12366  ennnfonelemkh  12367  ennnfonelemhf1o  12368  ennnfonelemhom  12370  nninfdclemlt  12406  fiinopn  12796  cnpfval  12989  iscnp3  12997  cnprcl2k  13000  tgcn  13002  lmbr  13007  lmbr2  13008  lmbrf  13009  lmss  13040  cnmptcom  13092  metss  13288  metcnp  13306  metcnpi  13309  metcnpi2  13310  elcncf  13354  cncfi  13359  rescncf  13362  cncfco  13372  cdivcncfap  13381  ellimc3apf  13423  limcdifap  13425  limcmpted  13426  limcimo  13428  limcresi  13429  cnplimclemr  13432  limccoap  13441  bdbm1.3ii  13926  bj-2inf  13973  bj-omtrans  13991  nninfalllem1  14041  nninfsellemdc  14043  nninfsellemqall  14048