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	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
imbi2d	⊢ (𝜑 → ((𝜃 → 𝜓) ↔ (𝜃 → 𝜒)))

Proof of Theorem imbi2d

Step	Hyp	Ref	Expression
1		imbid.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	a1d 22	. 2 ⊢ (𝜑 → (𝜃 → (𝜓 ↔ 𝜒)))
3	2	pm5.74d 182	1 ⊢ (𝜑 → ((𝜃 → 𝜓) ↔ (𝜃 → 𝜒)))

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  893  pm4.14dc  895  imimorbdc  901  pm5.6dc  931  ax11v2  1866  ax11v  1873  equs5or  1876  mo23  2119  nfabdw  2391  2gencl  2834  3gencl  2835  vtocl2gf  2864  vtocl3gf  2865  vtocl4g  2873  vtocl4ga  2874  eqeu  2974  mo2icl  2983  euind  2991  reu7  2999  reuind  3009  sbctt  3096  reu8nf  3111  sbcnestgf  3177  preq12bg  3852  elint  3930  elintrabg  3937  intab  3953  trss  4192  bm1.3ii  4206  pocl  4396  swopolem  4398  sowlin  4413  frforeq3  4440  frirrg  4443  frind  4445  reusv3  4553  regexmid  4629  ordsoexmid  4656  tfisi  4681  finds2  4695  nnregexmid  4715  vtoclr  4770  2optocl  4799  3optocl  4800  raliunxp  4867  resieq  5019  iss  5055  cnveqb  5188  iotaexab  5301  funmo  5337  fnbrfvb  5678  fvelimab  5696  fvmptssdm  5725  fmptco  5807  fnressn  5833  fressnfv  5834  isoselem  5954  isosolem  5958  ovg  6154  caovcan  6180  caovordig  6181  caovord  6187  f1o2ndf1  6386  poxp  6390  smoeq  6449  smores  6451  tfrlem1  6467  tfrlemi1  6491  tfrexlem  6493  tfri3  6526  oawordriexmid  6631  nnacl  6641  nnmcl  6642  nnacom  6645  nnaass  6646  nndi  6647  nnmass  6648  nnmsucr  6649  nnmcom  6650  nnsucsssuc  6653  nntri3or  6654  nnaordi  6669  nnaword  6672  nnmordi  6677  nnaordex  6689  2ecoptocl  6785  3ecoptocl  6786  th3qlem2  6800  xpdom2g  7009  findcard2  7069  findcard2s  7070  xpfi  7115  supeq1  7174  ordiso2  7223  updjud  7270  nnnninfeq  7316  exmidontriimlem4  7427  exmidontriim  7428  distrnq0  7667  addassnq0  7670  elinp  7682  prcdnql  7692  prcunqu  7693  prarloclem3  7705  caucvgpr  7890  caucvgprpr  7920  ltsosr  7972  caucvgsrlemcau  8001  caucvgsrlemgt1  8003  caucvgsrlemoffres  8008  pitonn  8056  axpre-ltwlin  8091  axcaucvglemres  8107  sup3exmid  9125  nnaddcl  9151  nnmulcl  9152  zaddcllempos  9504  zaddcllemneg  9506  prime  9567  peano5uzti  9576  uzind2  9580  zindd  9586  uzaddcl  9808  exfzdc  10474  infssuzex  10481  nninfdcex  10485  frec2uzltd  10653  frec2uzrdg  10659  frecuzrdgtcl  10662  frecuzrdgg  10666  frecuzrdgfunlem  10669  seq3val  10710  seqvalcd  10711  seq3clss  10721  seq3fveq2  10725  seqfveq2g  10727  seq3shft2  10731  seqshft2g  10732  monoord  10735  seq3split  10738  seqsplitg  10739  seq3caopr3  10741  seqcaopr3g  10742  seq3f1olemp  10765  seqf1oglem2a  10768  seqf1og  10771  seq3id3  10774  seq3id2  10776  seq3homo  10777  seq3z  10778  seqhomog  10780  seqfeq4g  10781  ser3ge0  10786  exp3vallem  10790  expcllem  10800  expap0  10819  mulexp  10828  expadd  10831  expmul  10834  leexp2r  10843  leexp1a  10844  bernneq  10910  modqexp  10916  nn0ltexp2  10959  apexp1  10968  facdiv  10988  faclbnd  10991  faclbnd6  10994  omgadd  11052  seq3coll  11093  wrdind  11290  wrd2ind  11291  pfxccatin12lem3  11300  shftvalg  11384  shftval4g  11385  cjexp  11441  resqrexlemover  11558  resqrexlemdecn  11560  resqrexlemlo  11561  resqrexlemcalc3  11564  absexp  11627  climshft  11852  climub  11892  climserle  11893  fsum2d  11983  fsumabs  12013  fsumiun  12025  binom  12032  bcxmas  12037  cvgratnnlemnexp  12072  cvgratnnlemmn  12073  clim2prod  12087  prodfap0  12093  prodfrecap  12094  fprodabs  12164  fprod2d  12171  demoivreALT  12322  dvdsfac  12408  bitsinv1  12510  bezoutlemstep  12555  bezoutlemmain  12556  bezoutlemex  12559  dfgcd2  12572  gcdmultiple  12578  rplpwr  12585  nn0seqcvgd  12600  alginv  12606  algcvga  12610  algfx  12611  isprm4  12678  prmind2  12679  prmdvdsexp  12707  prmfac1  12711  eulerthlemrprm  12788  eulerthlema  12789  reumodprminv  12813  pcmpt  12903  pcfac  12910  prmpwdvds  12915  ennnfoneleminc  13019  ennnfonelemkh  13020  ennnfonelemhf1o  13021  ennnfonelemhom  13023  nninfdclemlt  13059  gsumfzz  13565  mulgnnass  13731  mhmmulg  13737  gsumfzconst  13915  srgmulgass  13989  srgpcomp  13990  lmodvsmmulgdi  14324  cnfldexp  14578  gsumfzfsumlemm  14588  mplelbascoe  14693  fiinopn  14715  cnpfval  14906  iscnp3  14914  cnprcl2k  14917  tgcn  14919  lmbr  14924  lmbr2  14925  lmbrf  14926  lmss  14957  cnmptcom  15009  metss  15205  metcnp  15223  metcnpi  15226  metcnpi2  15227  elcncf  15284  cncfi  15289  rescncf  15292  cncfco  15302  cdivcncfap  15315  ellimc3apf  15371  limcdifap  15373  limcmpted  15374  limcimo  15376  limcresi  15377  cnplimclemr  15380  limccoap  15389  dvmptfsum  15436  plycolemc  15469  rpcxpmul2  15624  perfectlem2  15711  lgsquad2lem2  15798  bdbm1.3ii  16396  bj-2inf  16443  bj-omtrans  16461  nninfalllem1  16520  nninfsellemdc  16522  nninfsellemqall  16527