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  1843  ax11v  1850  equs5or  1853  mo23  2095  nfabdw  2367  2gencl  2805  3gencl  2806  vtocl2gf  2835  vtocl3gf  2836  eqeu  2943  mo2icl  2952  euind  2960  reu7  2968  reuind  2978  sbctt  3065  sbcnestgf  3145  preq12bg  3814  elint  3891  elintrabg  3898  intab  3914  trss  4152  bm1.3ii  4166  pocl  4351  swopolem  4353  sowlin  4368  frforeq3  4395  frirrg  4398  frind  4400  reusv3  4508  regexmid  4584  ordsoexmid  4611  tfisi  4636  finds2  4650  nnregexmid  4670  vtoclr  4724  2optocl  4753  3optocl  4754  raliunxp  4820  resieq  4970  iss  5006  cnveqb  5139  iotaexab  5251  funmo  5287  fnbrfvb  5621  fvelimab  5637  fvmptssdm  5666  fmptco  5748  fnressn  5772  fressnfv  5773  isoselem  5891  isosolem  5895  ovg  6087  caovcan  6113  caovordig  6114  caovord  6120  f1o2ndf1  6316  poxp  6320  smoeq  6378  smores  6380  tfrlem1  6396  tfrlemi1  6420  tfrexlem  6422  tfri3  6455  oawordriexmid  6558  nnacl  6568  nnmcl  6569  nnacom  6572  nnaass  6573  nndi  6574  nnmass  6575  nnmsucr  6576  nnmcom  6577  nnsucsssuc  6580  nntri3or  6581  nnaordi  6596  nnaword  6599  nnmordi  6604  nnaordex  6616  2ecoptocl  6712  3ecoptocl  6713  th3qlem2  6727  xpdom2g  6929  findcard2  6988  findcard2s  6989  xpfi  7031  supeq1  7090  ordiso2  7139  updjud  7186  nnnninfeq  7232  exmidontriimlem4  7338  exmidontriim  7339  distrnq0  7574  addassnq0  7577  elinp  7589  prcdnql  7599  prcunqu  7600  prarloclem3  7612  caucvgpr  7797  caucvgprpr  7827  ltsosr  7879  caucvgsrlemcau  7908  caucvgsrlemgt1  7910  caucvgsrlemoffres  7915  pitonn  7963  axpre-ltwlin  7998  axcaucvglemres  8014  sup3exmid  9032  nnaddcl  9058  nnmulcl  9059  zaddcllempos  9411  zaddcllemneg  9413  prime  9474  peano5uzti  9483  uzind2  9487  zindd  9493  uzaddcl  9709  exfzdc  10371  infssuzex  10378  nninfdcex  10382  frec2uzltd  10550  frec2uzrdg  10556  frecuzrdgtcl  10559  frecuzrdgg  10563  frecuzrdgfunlem  10566  seq3val  10607  seqvalcd  10608  seq3clss  10618  seq3fveq2  10622  seqfveq2g  10624  seq3shft2  10628  seqshft2g  10629  monoord  10632  seq3split  10635  seqsplitg  10636  seq3caopr3  10638  seqcaopr3g  10639  seq3f1olemp  10662  seqf1oglem2a  10665  seqf1og  10668  seq3id3  10671  seq3id2  10673  seq3homo  10674  seq3z  10675  seqhomog  10677  seqfeq4g  10678  ser3ge0  10683  exp3vallem  10687  expcllem  10697  expap0  10716  mulexp  10725  expadd  10728  expmul  10731  leexp2r  10740  leexp1a  10741  bernneq  10807  modqexp  10813  nn0ltexp2  10856  apexp1  10865  facdiv  10885  faclbnd  10888  faclbnd6  10891  omgadd  10949  seq3coll  10989  shftvalg  11180  shftval4g  11181  cjexp  11237  resqrexlemover  11354  resqrexlemdecn  11356  resqrexlemlo  11357  resqrexlemcalc3  11360  absexp  11423  climshft  11648  climub  11688  climserle  11689  fsum2d  11779  fsumabs  11809  fsumiun  11821  binom  11828  bcxmas  11833  cvgratnnlemnexp  11868  cvgratnnlemmn  11869  clim2prod  11883  prodfap0  11889  prodfrecap  11890  fprodabs  11960  fprod2d  11967  demoivreALT  12118  dvdsfac  12204  bitsinv1  12306  bezoutlemstep  12351  bezoutlemmain  12352  bezoutlemex  12355  dfgcd2  12368  gcdmultiple  12374  rplpwr  12381  nn0seqcvgd  12396  alginv  12402  algcvga  12406  algfx  12407  isprm4  12474  prmind2  12475  prmdvdsexp  12503  prmfac1  12507  eulerthlemrprm  12584  eulerthlema  12585  reumodprminv  12609  pcmpt  12699  pcfac  12706  prmpwdvds  12711  ennnfoneleminc  12815  ennnfonelemkh  12816  ennnfonelemhf1o  12817  ennnfonelemhom  12819  nninfdclemlt  12855  gsumfzz  13360  mulgnnass  13526  mhmmulg  13532  gsumfzconst  13710  srgmulgass  13784  srgpcomp  13785  lmodvsmmulgdi  14118  cnfldexp  14372  gsumfzfsumlemm  14382  mplelbascoe  14487  fiinopn  14509  cnpfval  14700  iscnp3  14708  cnprcl2k  14711  tgcn  14713  lmbr  14718  lmbr2  14719  lmbrf  14720  lmss  14751  cnmptcom  14803  metss  14999  metcnp  15017  metcnpi  15020  metcnpi2  15021  elcncf  15078  cncfi  15083  rescncf  15086  cncfco  15096  cdivcncfap  15109  ellimc3apf  15165  limcdifap  15167  limcmpted  15168  limcimo  15170  limcresi  15171  cnplimclemr  15174  limccoap  15183  dvmptfsum  15230  plycolemc  15263  rpcxpmul2  15418  perfectlem2  15505  lgsquad2lem2  15592  bdbm1.3ii  15864  bj-2inf  15911  bj-omtrans  15929  nninfalllem1  15982  nninfsellemdc  15984  nninfsellemqall  15989