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  1831  ax11v  1838  equs5or  1841  mo23  2083  nfabdw  2355  2gencl  2793  3gencl  2794  vtocl2gf  2823  vtocl3gf  2824  eqeu  2931  mo2icl  2940  euind  2948  reu7  2956  reuind  2966  sbctt  3053  sbcnestgf  3133  preq12bg  3800  elint  3877  elintrabg  3884  intab  3900  trss  4137  bm1.3ii  4151  pocl  4335  swopolem  4337  sowlin  4352  frforeq3  4379  frirrg  4382  frind  4384  reusv3  4492  regexmid  4568  ordsoexmid  4595  tfisi  4620  finds2  4634  nnregexmid  4654  vtoclr  4708  2optocl  4737  3optocl  4738  raliunxp  4804  resieq  4953  iss  4989  cnveqb  5122  iotaexab  5234  funmo  5270  fnbrfvb  5598  fvelimab  5614  fvmptssdm  5643  fmptco  5725  fnressn  5745  fressnfv  5746  isoselem  5864  isosolem  5868  ovg  6059  caovcan  6085  caovordig  6086  caovord  6092  f1o2ndf1  6283  poxp  6287  smoeq  6345  smores  6347  tfrlem1  6363  tfrlemi1  6387  tfrexlem  6389  tfri3  6422  oawordriexmid  6525  nnacl  6535  nnmcl  6536  nnacom  6539  nnaass  6540  nndi  6541  nnmass  6542  nnmsucr  6543  nnmcom  6544  nnsucsssuc  6547  nntri3or  6548  nnaordi  6563  nnaword  6566  nnmordi  6571  nnaordex  6583  2ecoptocl  6679  3ecoptocl  6680  th3qlem2  6694  xpdom2g  6888  findcard2  6947  findcard2s  6948  xpfi  6988  supeq1  7047  ordiso2  7096  updjud  7143  nnnninfeq  7189  exmidontriimlem4  7286  exmidontriim  7287  distrnq0  7521  addassnq0  7524  elinp  7536  prcdnql  7546  prcunqu  7547  prarloclem3  7559  caucvgpr  7744  caucvgprpr  7774  ltsosr  7826  caucvgsrlemcau  7855  caucvgsrlemgt1  7857  caucvgsrlemoffres  7862  pitonn  7910  axpre-ltwlin  7945  axcaucvglemres  7961  sup3exmid  8978  nnaddcl  9004  nnmulcl  9005  zaddcllempos  9357  zaddcllemneg  9359  prime  9419  peano5uzti  9428  uzind2  9432  zindd  9438  uzaddcl  9654  exfzdc  10310  frec2uzltd  10477  frec2uzrdg  10483  frecuzrdgtcl  10486  frecuzrdgg  10490  frecuzrdgfunlem  10493  seq3val  10534  seqvalcd  10535  seq3clss  10545  seq3fveq2  10549  seqfveq2g  10551  seq3shft2  10555  seqshft2g  10556  monoord  10559  seq3split  10562  seqsplitg  10563  seq3caopr3  10565  seqcaopr3g  10566  seq3f1olemp  10589  seqf1oglem2a  10592  seqf1og  10595  seq3id3  10598  seq3id2  10600  seq3homo  10601  seq3z  10602  seqhomog  10604  seqfeq4g  10605  ser3ge0  10610  exp3vallem  10614  expcllem  10624  expap0  10643  mulexp  10652  expadd  10655  expmul  10658  leexp2r  10667  leexp1a  10668  bernneq  10734  modqexp  10740  nn0ltexp2  10783  apexp1  10792  facdiv  10812  faclbnd  10815  faclbnd6  10818  omgadd  10876  seq3coll  10916  shftvalg  10983  shftval4g  10984  cjexp  11040  resqrexlemover  11157  resqrexlemdecn  11159  resqrexlemlo  11160  resqrexlemcalc3  11163  absexp  11226  climshft  11450  climub  11490  climserle  11491  fsum2d  11581  fsumabs  11611  fsumiun  11623  binom  11630  bcxmas  11635  cvgratnnlemnexp  11670  cvgratnnlemmn  11671  clim2prod  11685  prodfap0  11691  prodfrecap  11692  fprodabs  11762  fprod2d  11769  demoivreALT  11920  dvdsfac  12005  infssuzex  12089  nninfdcex  12093  bezoutlemstep  12137  bezoutlemmain  12138  bezoutlemex  12141  dfgcd2  12154  gcdmultiple  12160  rplpwr  12167  nn0seqcvgd  12182  alginv  12188  algcvga  12192  algfx  12193  isprm4  12260  prmind2  12261  prmdvdsexp  12289  prmfac1  12293  eulerthlemrprm  12370  eulerthlema  12371  reumodprminv  12394  pcmpt  12484  pcfac  12491  prmpwdvds  12496  ennnfoneleminc  12571  ennnfonelemkh  12572  ennnfonelemhf1o  12573  ennnfonelemhom  12575  nninfdclemlt  12611  gsumfzz  13070  mulgnnass  13230  mhmmulg  13236  gsumfzconst  13414  srgmulgass  13488  srgpcomp  13489  lmodvsmmulgdi  13822  cnfldexp  14076  gsumfzfsumlemm  14086  fiinopn  14183  cnpfval  14374  iscnp3  14382  cnprcl2k  14385  tgcn  14387  lmbr  14392  lmbr2  14393  lmbrf  14394  lmss  14425  cnmptcom  14477  metss  14673  metcnp  14691  metcnpi  14694  metcnpi2  14695  elcncf  14752  cncfi  14757  rescncf  14760  cncfco  14770  cdivcncfap  14783  ellimc3apf  14839  limcdifap  14841  limcmpted  14842  limcimo  14844  limcresi  14845  cnplimclemr  14848  limccoap  14857  dvmptfsum  14904  plycolemc  14936  lgsquad2lem2  15239  bdbm1.3ii  15453  bj-2inf  15500  bj-omtrans  15518  nninfalllem1  15568  nninfsellemdc  15570  nninfsellemqall  15575