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  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  3804  elint  3881  elintrabg  3888  intab  3904  trss  4141  bm1.3ii  4155  pocl  4339  swopolem  4341  sowlin  4356  frforeq3  4383  frirrg  4386  frind  4388  reusv3  4496  regexmid  4572  ordsoexmid  4599  tfisi  4624  finds2  4638  nnregexmid  4658  vtoclr  4712  2optocl  4741  3optocl  4742  raliunxp  4808  resieq  4957  iss  4993  cnveqb  5126  iotaexab  5238  funmo  5274  fnbrfvb  5604  fvelimab  5620  fvmptssdm  5649  fmptco  5731  fnressn  5751  fressnfv  5752  isoselem  5870  isosolem  5874  ovg  6066  caovcan  6092  caovordig  6093  caovord  6099  f1o2ndf1  6295  poxp  6299  smoeq  6357  smores  6359  tfrlem1  6375  tfrlemi1  6399  tfrexlem  6401  tfri3  6434  oawordriexmid  6537  nnacl  6547  nnmcl  6548  nnacom  6551  nnaass  6552  nndi  6553  nnmass  6554  nnmsucr  6555  nnmcom  6556  nnsucsssuc  6559  nntri3or  6560  nnaordi  6575  nnaword  6578  nnmordi  6583  nnaordex  6595  2ecoptocl  6691  3ecoptocl  6692  th3qlem2  6706  xpdom2g  6900  findcard2  6959  findcard2s  6960  xpfi  7002  supeq1  7061  ordiso2  7110  updjud  7157  nnnninfeq  7203  exmidontriimlem4  7309  exmidontriim  7310  distrnq0  7545  addassnq0  7548  elinp  7560  prcdnql  7570  prcunqu  7571  prarloclem3  7583  caucvgpr  7768  caucvgprpr  7798  ltsosr  7850  caucvgsrlemcau  7879  caucvgsrlemgt1  7881  caucvgsrlemoffres  7886  pitonn  7934  axpre-ltwlin  7969  axcaucvglemres  7985  sup3exmid  9003  nnaddcl  9029  nnmulcl  9030  zaddcllempos  9382  zaddcllemneg  9384  prime  9444  peano5uzti  9453  uzind2  9457  zindd  9463  uzaddcl  9679  exfzdc  10335  infssuzex  10342  nninfdcex  10346  frec2uzltd  10514  frec2uzrdg  10520  frecuzrdgtcl  10523  frecuzrdgg  10527  frecuzrdgfunlem  10530  seq3val  10571  seqvalcd  10572  seq3clss  10582  seq3fveq2  10586  seqfveq2g  10588  seq3shft2  10592  seqshft2g  10593  monoord  10596  seq3split  10599  seqsplitg  10600  seq3caopr3  10602  seqcaopr3g  10603  seq3f1olemp  10626  seqf1oglem2a  10629  seqf1og  10632  seq3id3  10635  seq3id2  10637  seq3homo  10638  seq3z  10639  seqhomog  10641  seqfeq4g  10642  ser3ge0  10647  exp3vallem  10651  expcllem  10661  expap0  10680  mulexp  10689  expadd  10692  expmul  10695  leexp2r  10704  leexp1a  10705  bernneq  10771  modqexp  10777  nn0ltexp2  10820  apexp1  10829  facdiv  10849  faclbnd  10852  faclbnd6  10855  omgadd  10913  seq3coll  10953  shftvalg  11020  shftval4g  11021  cjexp  11077  resqrexlemover  11194  resqrexlemdecn  11196  resqrexlemlo  11197  resqrexlemcalc3  11200  absexp  11263  climshft  11488  climub  11528  climserle  11529  fsum2d  11619  fsumabs  11649  fsumiun  11661  binom  11668  bcxmas  11673  cvgratnnlemnexp  11708  cvgratnnlemmn  11709  clim2prod  11723  prodfap0  11729  prodfrecap  11730  fprodabs  11800  fprod2d  11807  demoivreALT  11958  dvdsfac  12044  bitsinv1  12146  bezoutlemstep  12191  bezoutlemmain  12192  bezoutlemex  12195  dfgcd2  12208  gcdmultiple  12214  rplpwr  12221  nn0seqcvgd  12236  alginv  12242  algcvga  12246  algfx  12247  isprm4  12314  prmind2  12315  prmdvdsexp  12343  prmfac1  12347  eulerthlemrprm  12424  eulerthlema  12425  reumodprminv  12449  pcmpt  12539  pcfac  12546  prmpwdvds  12551  ennnfoneleminc  12655  ennnfonelemkh  12656  ennnfonelemhf1o  12657  ennnfonelemhom  12659  nninfdclemlt  12695  gsumfzz  13199  mulgnnass  13365  mhmmulg  13371  gsumfzconst  13549  srgmulgass  13623  srgpcomp  13624  lmodvsmmulgdi  13957  cnfldexp  14211  gsumfzfsumlemm  14221  mplelbascoe  14326  fiinopn  14348  cnpfval  14539  iscnp3  14547  cnprcl2k  14550  tgcn  14552  lmbr  14557  lmbr2  14558  lmbrf  14559  lmss  14590  cnmptcom  14642  metss  14838  metcnp  14856  metcnpi  14859  metcnpi2  14860  elcncf  14917  cncfi  14922  rescncf  14925  cncfco  14935  cdivcncfap  14948  ellimc3apf  15004  limcdifap  15006  limcmpted  15007  limcimo  15009  limcresi  15010  cnplimclemr  15013  limccoap  15022  dvmptfsum  15069  plycolemc  15102  rpcxpmul2  15257  perfectlem2  15344  lgsquad2lem2  15431  bdbm1.3ii  15645  bj-2inf  15692  bj-omtrans  15710  nninfalllem1  15763  nninfsellemdc  15765  nninfsellemqall  15770