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  896  pm4.14dc  898  imimorbdc  904  pm5.6dc  934  ax11v2  1868  ax11v  1875  equs5or  1878  mo23  2121  nfabdw  2394  2gencl  2837  3gencl  2838  vtocl2gf  2867  vtocl3gf  2868  vtocl4g  2876  vtocl4ga  2877  eqeu  2977  mo2icl  2986  euind  2994  reu7  3002  reuind  3012  sbctt  3099  reu8nf  3114  sbcnestgf  3180  preq12bg  3861  elint  3939  elintrabg  3946  intab  3962  trss  4201  bm1.3ii  4215  pocl  4406  swopolem  4408  sowlin  4423  frforeq3  4450  frirrg  4453  frind  4455  reusv3  4563  regexmid  4639  ordsoexmid  4666  tfisi  4691  finds2  4705  nnregexmid  4725  vtoclr  4780  2optocl  4809  3optocl  4810  raliunxp  4877  resieq  5029  iss  5065  cnveqb  5199  iotaexab  5312  funmo  5348  fnbrfvb  5693  fvelimab  5711  fvmptssdm  5740  fmptco  5821  fnressn  5848  fressnfv  5849  isoselem  5971  isosolem  5975  ovg  6171  caovcan  6197  caovordig  6198  caovord  6204  f1o2ndf1  6402  poxp  6406  smoeq  6499  smores  6501  tfrlem1  6517  tfrlemi1  6541  tfrexlem  6543  tfri3  6576  oawordriexmid  6681  nnacl  6691  nnmcl  6692  nnacom  6695  nnaass  6696  nndi  6697  nnmass  6698  nnmsucr  6699  nnmcom  6700  nnsucsssuc  6703  nntri3or  6704  nnaordi  6719  nnaword  6722  nnmordi  6727  nnaordex  6739  2ecoptocl  6835  3ecoptocl  6836  th3qlem2  6850  xpdom2g  7059  findcard2  7121  findcard2s  7122  xpfi  7167  supeq1  7228  ordiso2  7277  updjud  7324  nnnninfeq  7370  exmidontriimlem4  7482  exmidontriim  7483  distrnq0  7722  addassnq0  7725  elinp  7737  prcdnql  7747  prcunqu  7748  prarloclem3  7760  caucvgpr  7945  caucvgprpr  7975  ltsosr  8027  caucvgsrlemcau  8056  caucvgsrlemgt1  8058  caucvgsrlemoffres  8063  pitonn  8111  axpre-ltwlin  8146  axcaucvglemres  8162  sup3exmid  9180  nnaddcl  9206  nnmulcl  9207  zaddcllempos  9559  zaddcllemneg  9561  prime  9622  peano5uzti  9631  uzind2  9635  zindd  9641  uzaddcl  9863  exfzdc  10530  infssuzex  10537  nninfdcex  10541  frec2uzltd  10709  frec2uzrdg  10715  frecuzrdgtcl  10718  frecuzrdgg  10722  frecuzrdgfunlem  10725  seq3val  10766  seqvalcd  10767  seq3clss  10777  seq3fveq2  10781  seqfveq2g  10783  seq3shft2  10787  seqshft2g  10788  monoord  10791  seq3split  10794  seqsplitg  10795  seq3caopr3  10797  seqcaopr3g  10798  seq3f1olemp  10821  seqf1oglem2a  10824  seqf1og  10827  seq3id3  10830  seq3id2  10832  seq3homo  10833  seq3z  10834  seqhomog  10836  seqfeq4g  10837  ser3ge0  10842  exp3vallem  10846  expcllem  10856  expap0  10875  mulexp  10884  expadd  10887  expmul  10890  leexp2r  10899  leexp1a  10900  bernneq  10966  modqexp  10972  nn0ltexp2  11015  apexp1  11024  facdiv  11044  faclbnd  11047  faclbnd6  11050  omgadd  11109  seq3coll  11150  wrdind  11350  wrd2ind  11351  pfxccatin12lem3  11360  shftvalg  11457  shftval4g  11458  cjexp  11514  resqrexlemover  11631  resqrexlemdecn  11633  resqrexlemlo  11634  resqrexlemcalc3  11637  absexp  11700  climshft  11925  climub  11965  climserle  11966  fsum2d  12057  fsumabs  12087  fsumiun  12099  binom  12106  bcxmas  12111  cvgratnnlemnexp  12146  cvgratnnlemmn  12147  clim2prod  12161  prodfap0  12167  prodfrecap  12168  fprodabs  12238  fprod2d  12245  demoivreALT  12396  dvdsfac  12482  bitsinv1  12584  bezoutlemstep  12629  bezoutlemmain  12630  bezoutlemex  12633  dfgcd2  12646  gcdmultiple  12652  rplpwr  12659  nn0seqcvgd  12674  alginv  12680  algcvga  12684  algfx  12685  isprm4  12752  prmind2  12753  prmdvdsexp  12781  prmfac1  12785  eulerthlemrprm  12862  eulerthlema  12863  reumodprminv  12887  pcmpt  12977  pcfac  12984  prmpwdvds  12989  ennnfoneleminc  13093  ennnfonelemkh  13094  ennnfonelemhf1o  13095  ennnfonelemhom  13097  nninfdclemlt  13133  gsumfzz  13639  mulgnnass  13805  mhmmulg  13811  gsumfzconst  13989  srgmulgass  14064  srgpcomp  14065  lmodvsmmulgdi  14399  cnfldexp  14653  gsumfzfsumlemm  14663  mplelbascoe  14773  fiinopn  14795  cnpfval  14986  iscnp3  14994  cnprcl2k  14997  tgcn  14999  lmbr  15004  lmbr2  15005  lmbrf  15006  lmss  15037  cnmptcom  15089  metss  15285  metcnp  15303  metcnpi  15306  metcnpi2  15307  elcncf  15364  cncfi  15369  rescncf  15372  cncfco  15382  cdivcncfap  15395  ellimc3apf  15451  limcdifap  15453  limcmpted  15454  limcimo  15456  limcresi  15457  cnplimclemr  15460  limccoap  15469  dvmptfsum  15516  plycolemc  15549  rpcxpmul2  15704  perfectlem2  15794  lgsquad2lem2  15881  eupth2fi  16400  depindlem2  16428  depindlem3  16429  bdbm1.3ii  16587  bj-2inf  16634  bj-omtrans  16652  exmidcon  16708  exmidpeirce  16709  nninfalllem1  16714  nninfsellemdc  16716  nninfsellemqall  16721