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  889  pm4.14dc  891  imimorbdc  897  pm5.6dc  927  ax11v2  1834  ax11v  1841  equs5or  1844  mo23  2086  nfabdw  2358  2gencl  2796  3gencl  2797  vtocl2gf  2826  vtocl3gf  2827  eqeu  2934  mo2icl  2943  euind  2951  reu7  2959  reuind  2969  sbctt  3056  sbcnestgf  3136  preq12bg  3803  elint  3880  elintrabg  3887  intab  3903  trss  4140  bm1.3ii  4154  pocl  4338  swopolem  4340  sowlin  4355  frforeq3  4382  frirrg  4385  frind  4387  reusv3  4495  regexmid  4571  ordsoexmid  4598  tfisi  4623  finds2  4637  nnregexmid  4657  vtoclr  4711  2optocl  4740  3optocl  4741  raliunxp  4807  resieq  4956  iss  4992  cnveqb  5125  iotaexab  5237  funmo  5273  fnbrfvb  5601  fvelimab  5617  fvmptssdm  5646  fmptco  5728  fnressn  5748  fressnfv  5749  isoselem  5867  isosolem  5871  ovg  6062  caovcan  6088  caovordig  6089  caovord  6095  f1o2ndf1  6286  poxp  6290  smoeq  6348  smores  6350  tfrlem1  6366  tfrlemi1  6390  tfrexlem  6392  tfri3  6425  oawordriexmid  6528  nnacl  6538  nnmcl  6539  nnacom  6542  nnaass  6543  nndi  6544  nnmass  6545  nnmsucr  6546  nnmcom  6547  nnsucsssuc  6550  nntri3or  6551  nnaordi  6566  nnaword  6569  nnmordi  6574  nnaordex  6586  2ecoptocl  6682  3ecoptocl  6683  th3qlem2  6697  xpdom2g  6891  findcard2  6950  findcard2s  6951  xpfi  6993  supeq1  7052  ordiso2  7101  updjud  7148  nnnninfeq  7194  exmidontriimlem4  7291  exmidontriim  7292  distrnq0  7526  addassnq0  7529  elinp  7541  prcdnql  7551  prcunqu  7552  prarloclem3  7564  caucvgpr  7749  caucvgprpr  7779  ltsosr  7831  caucvgsrlemcau  7860  caucvgsrlemgt1  7862  caucvgsrlemoffres  7867  pitonn  7915  axpre-ltwlin  7950  axcaucvglemres  7966  sup3exmid  8984  nnaddcl  9010  nnmulcl  9011  zaddcllempos  9363  zaddcllemneg  9365  prime  9425  peano5uzti  9434  uzind2  9438  zindd  9444  uzaddcl  9660  exfzdc  10316  infssuzex  10323  nninfdcex  10327  frec2uzltd  10495  frec2uzrdg  10501  frecuzrdgtcl  10504  frecuzrdgg  10508  frecuzrdgfunlem  10511  seq3val  10552  seqvalcd  10553  seq3clss  10563  seq3fveq2  10567  seqfveq2g  10569  seq3shft2  10573  seqshft2g  10574  monoord  10577  seq3split  10580  seqsplitg  10581  seq3caopr3  10583  seqcaopr3g  10584  seq3f1olemp  10607  seqf1oglem2a  10610  seqf1og  10613  seq3id3  10616  seq3id2  10618  seq3homo  10619  seq3z  10620  seqhomog  10622  seqfeq4g  10623  ser3ge0  10628  exp3vallem  10632  expcllem  10642  expap0  10661  mulexp  10670  expadd  10673  expmul  10676  leexp2r  10685  leexp1a  10686  bernneq  10752  modqexp  10758  nn0ltexp2  10801  apexp1  10810  facdiv  10830  faclbnd  10833  faclbnd6  10836  omgadd  10894  seq3coll  10934  shftvalg  11001  shftval4g  11002  cjexp  11058  resqrexlemover  11175  resqrexlemdecn  11177  resqrexlemlo  11178  resqrexlemcalc3  11181  absexp  11244  climshft  11469  climub  11509  climserle  11510  fsum2d  11600  fsumabs  11630  fsumiun  11642  binom  11649  bcxmas  11654  cvgratnnlemnexp  11689  cvgratnnlemmn  11690  clim2prod  11704  prodfap0  11710  prodfrecap  11711  fprodabs  11781  fprod2d  11788  demoivreALT  11939  dvdsfac  12025  bezoutlemstep  12164  bezoutlemmain  12165  bezoutlemex  12168  dfgcd2  12181  gcdmultiple  12187  rplpwr  12194  nn0seqcvgd  12209  alginv  12215  algcvga  12219  algfx  12220  isprm4  12287  prmind2  12288  prmdvdsexp  12316  prmfac1  12320  eulerthlemrprm  12397  eulerthlema  12398  reumodprminv  12422  pcmpt  12512  pcfac  12519  prmpwdvds  12524  ennnfoneleminc  12628  ennnfonelemkh  12629  ennnfonelemhf1o  12630  ennnfonelemhom  12632  nninfdclemlt  12668  gsumfzz  13127  mulgnnass  13287  mhmmulg  13293  gsumfzconst  13471  srgmulgass  13545  srgpcomp  13546  lmodvsmmulgdi  13879  cnfldexp  14133  gsumfzfsumlemm  14143  fiinopn  14240  cnpfval  14431  iscnp3  14439  cnprcl2k  14442  tgcn  14444  lmbr  14449  lmbr2  14450  lmbrf  14451  lmss  14482  cnmptcom  14534  metss  14730  metcnp  14748  metcnpi  14751  metcnpi2  14752  elcncf  14809  cncfi  14814  rescncf  14817  cncfco  14827  cdivcncfap  14840  ellimc3apf  14896  limcdifap  14898  limcmpted  14899  limcimo  14901  limcresi  14902  cnplimclemr  14905  limccoap  14914  dvmptfsum  14961  plycolemc  14994  rpcxpmul2  15149  perfectlem2  15236  lgsquad2lem2  15323  bdbm1.3ii  15537  bj-2inf  15584  bj-omtrans  15602  nninfalllem1  15652  nninfsellemdc  15654  nninfsellemqall  15659