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  2833  3gencl  2834  vtocl2gf  2863  vtocl3gf  2864  vtocl4g  2872  vtocl4ga  2873  eqeu  2973  mo2icl  2982  euind  2990  reu7  2998  reuind  3008  sbctt  3095  reu8nf  3110  sbcnestgf  3176  preq12bg  3851  elint  3929  elintrabg  3936  intab  3952  trss  4191  bm1.3ii  4205  pocl  4394  swopolem  4396  sowlin  4411  frforeq3  4438  frirrg  4441  frind  4443  reusv3  4551  regexmid  4627  ordsoexmid  4654  tfisi  4679  finds2  4693  nnregexmid  4713  vtoclr  4767  2optocl  4796  3optocl  4797  raliunxp  4863  resieq  5015  iss  5051  cnveqb  5184  iotaexab  5297  funmo  5333  fnbrfvb  5674  fvelimab  5692  fvmptssdm  5721  fmptco  5803  fnressn  5829  fressnfv  5830  isoselem  5950  isosolem  5954  ovg  6150  caovcan  6176  caovordig  6177  caovord  6183  f1o2ndf1  6380  poxp  6384  smoeq  6442  smores  6444  tfrlem1  6460  tfrlemi1  6484  tfrexlem  6486  tfri3  6519  oawordriexmid  6624  nnacl  6634  nnmcl  6635  nnacom  6638  nnaass  6639  nndi  6640  nnmass  6641  nnmsucr  6642  nnmcom  6643  nnsucsssuc  6646  nntri3or  6647  nnaordi  6662  nnaword  6665  nnmordi  6670  nnaordex  6682  2ecoptocl  6778  3ecoptocl  6779  th3qlem2  6793  xpdom2g  6999  findcard2  7059  findcard2s  7060  xpfi  7102  supeq1  7161  ordiso2  7210  updjud  7257  nnnninfeq  7303  exmidontriimlem4  7414  exmidontriim  7415  distrnq0  7654  addassnq0  7657  elinp  7669  prcdnql  7679  prcunqu  7680  prarloclem3  7692  caucvgpr  7877  caucvgprpr  7907  ltsosr  7959  caucvgsrlemcau  7988  caucvgsrlemgt1  7990  caucvgsrlemoffres  7995  pitonn  8043  axpre-ltwlin  8078  axcaucvglemres  8094  sup3exmid  9112  nnaddcl  9138  nnmulcl  9139  zaddcllempos  9491  zaddcllemneg  9493  prime  9554  peano5uzti  9563  uzind2  9567  zindd  9573  uzaddcl  9789  exfzdc  10454  infssuzex  10461  nninfdcex  10465  frec2uzltd  10633  frec2uzrdg  10639  frecuzrdgtcl  10642  frecuzrdgg  10646  frecuzrdgfunlem  10649  seq3val  10690  seqvalcd  10691  seq3clss  10701  seq3fveq2  10705  seqfveq2g  10707  seq3shft2  10711  seqshft2g  10712  monoord  10715  seq3split  10718  seqsplitg  10719  seq3caopr3  10721  seqcaopr3g  10722  seq3f1olemp  10745  seqf1oglem2a  10748  seqf1og  10751  seq3id3  10754  seq3id2  10756  seq3homo  10757  seq3z  10758  seqhomog  10760  seqfeq4g  10761  ser3ge0  10766  exp3vallem  10770  expcllem  10780  expap0  10799  mulexp  10808  expadd  10811  expmul  10814  leexp2r  10823  leexp1a  10824  bernneq  10890  modqexp  10896  nn0ltexp2  10939  apexp1  10948  facdiv  10968  faclbnd  10971  faclbnd6  10974  omgadd  11032  seq3coll  11072  wrdind  11262  wrd2ind  11263  pfxccatin12lem3  11272  shftvalg  11355  shftval4g  11356  cjexp  11412  resqrexlemover  11529  resqrexlemdecn  11531  resqrexlemlo  11532  resqrexlemcalc3  11535  absexp  11598  climshft  11823  climub  11863  climserle  11864  fsum2d  11954  fsumabs  11984  fsumiun  11996  binom  12003  bcxmas  12008  cvgratnnlemnexp  12043  cvgratnnlemmn  12044  clim2prod  12058  prodfap0  12064  prodfrecap  12065  fprodabs  12135  fprod2d  12142  demoivreALT  12293  dvdsfac  12379  bitsinv1  12481  bezoutlemstep  12526  bezoutlemmain  12527  bezoutlemex  12530  dfgcd2  12543  gcdmultiple  12549  rplpwr  12556  nn0seqcvgd  12571  alginv  12577  algcvga  12581  algfx  12582  isprm4  12649  prmind2  12650  prmdvdsexp  12678  prmfac1  12682  eulerthlemrprm  12759  eulerthlema  12760  reumodprminv  12784  pcmpt  12874  pcfac  12881  prmpwdvds  12886  ennnfoneleminc  12990  ennnfonelemkh  12991  ennnfonelemhf1o  12992  ennnfonelemhom  12994  nninfdclemlt  13030  gsumfzz  13536  mulgnnass  13702  mhmmulg  13708  gsumfzconst  13886  srgmulgass  13960  srgpcomp  13961  lmodvsmmulgdi  14295  cnfldexp  14549  gsumfzfsumlemm  14559  mplelbascoe  14664  fiinopn  14686  cnpfval  14877  iscnp3  14885  cnprcl2k  14888  tgcn  14890  lmbr  14895  lmbr2  14896  lmbrf  14897  lmss  14928  cnmptcom  14980  metss  15176  metcnp  15194  metcnpi  15197  metcnpi2  15198  elcncf  15255  cncfi  15260  rescncf  15263  cncfco  15273  cdivcncfap  15286  ellimc3apf  15342  limcdifap  15344  limcmpted  15345  limcimo  15347  limcresi  15348  cnplimclemr  15351  limccoap  15360  dvmptfsum  15407  plycolemc  15440  rpcxpmul2  15595  perfectlem2  15682  lgsquad2lem2  15769  bdbm1.3ii  16278  bj-2inf  16325  bj-omtrans  16343  nninfalllem1  16404  nninfsellemdc  16406  nninfsellemqall  16411