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  4395  swopolem  4397  sowlin  4412  frforeq3  4439  frirrg  4442  frind  4444  reusv3  4552  regexmid  4628  ordsoexmid  4655  tfisi  4680  finds2  4694  nnregexmid  4714  vtoclr  4769  2optocl  4798  3optocl  4799  raliunxp  4866  resieq  5018  iss  5054  cnveqb  5187  iotaexab  5300  funmo  5336  fnbrfvb  5677  fvelimab  5695  fvmptssdm  5724  fmptco  5806  fnressn  5832  fressnfv  5833  isoselem  5953  isosolem  5957  ovg  6153  caovcan  6179  caovordig  6180  caovord  6186  f1o2ndf1  6385  poxp  6389  smoeq  6447  smores  6449  tfrlem1  6465  tfrlemi1  6489  tfrexlem  6491  tfri3  6524  oawordriexmid  6629  nnacl  6639  nnmcl  6640  nnacom  6643  nnaass  6644  nndi  6645  nnmass  6646  nnmsucr  6647  nnmcom  6648  nnsucsssuc  6651  nntri3or  6652  nnaordi  6667  nnaword  6670  nnmordi  6675  nnaordex  6687  2ecoptocl  6783  3ecoptocl  6784  th3qlem2  6798  xpdom2g  7004  findcard2  7064  findcard2s  7065  xpfi  7110  supeq1  7169  ordiso2  7218  updjud  7265  nnnninfeq  7311  exmidontriimlem4  7422  exmidontriim  7423  distrnq0  7662  addassnq0  7665  elinp  7677  prcdnql  7687  prcunqu  7688  prarloclem3  7700  caucvgpr  7885  caucvgprpr  7915  ltsosr  7967  caucvgsrlemcau  7996  caucvgsrlemgt1  7998  caucvgsrlemoffres  8003  pitonn  8051  axpre-ltwlin  8086  axcaucvglemres  8102  sup3exmid  9120  nnaddcl  9146  nnmulcl  9147  zaddcllempos  9499  zaddcllemneg  9501  prime  9562  peano5uzti  9571  uzind2  9575  zindd  9581  uzaddcl  9798  exfzdc  10463  infssuzex  10470  nninfdcex  10474  frec2uzltd  10642  frec2uzrdg  10648  frecuzrdgtcl  10651  frecuzrdgg  10655  frecuzrdgfunlem  10658  seq3val  10699  seqvalcd  10700  seq3clss  10710  seq3fveq2  10714  seqfveq2g  10716  seq3shft2  10720  seqshft2g  10721  monoord  10724  seq3split  10727  seqsplitg  10728  seq3caopr3  10730  seqcaopr3g  10731  seq3f1olemp  10754  seqf1oglem2a  10757  seqf1og  10760  seq3id3  10763  seq3id2  10765  seq3homo  10766  seq3z  10767  seqhomog  10769  seqfeq4g  10770  ser3ge0  10775  exp3vallem  10779  expcllem  10789  expap0  10808  mulexp  10817  expadd  10820  expmul  10823  leexp2r  10832  leexp1a  10833  bernneq  10899  modqexp  10905  nn0ltexp2  10948  apexp1  10957  facdiv  10977  faclbnd  10980  faclbnd6  10983  omgadd  11041  seq3coll  11082  wrdind  11275  wrd2ind  11276  pfxccatin12lem3  11285  shftvalg  11368  shftval4g  11369  cjexp  11425  resqrexlemover  11542  resqrexlemdecn  11544  resqrexlemlo  11545  resqrexlemcalc3  11548  absexp  11611  climshft  11836  climub  11876  climserle  11877  fsum2d  11967  fsumabs  11997  fsumiun  12009  binom  12016  bcxmas  12021  cvgratnnlemnexp  12056  cvgratnnlemmn  12057  clim2prod  12071  prodfap0  12077  prodfrecap  12078  fprodabs  12148  fprod2d  12155  demoivreALT  12306  dvdsfac  12392  bitsinv1  12494  bezoutlemstep  12539  bezoutlemmain  12540  bezoutlemex  12543  dfgcd2  12556  gcdmultiple  12562  rplpwr  12569  nn0seqcvgd  12584  alginv  12590  algcvga  12594  algfx  12595  isprm4  12662  prmind2  12663  prmdvdsexp  12691  prmfac1  12695  eulerthlemrprm  12772  eulerthlema  12773  reumodprminv  12797  pcmpt  12887  pcfac  12894  prmpwdvds  12899  ennnfoneleminc  13003  ennnfonelemkh  13004  ennnfonelemhf1o  13005  ennnfonelemhom  13007  nninfdclemlt  13043  gsumfzz  13549  mulgnnass  13715  mhmmulg  13721  gsumfzconst  13899  srgmulgass  13973  srgpcomp  13974  lmodvsmmulgdi  14308  cnfldexp  14562  gsumfzfsumlemm  14572  mplelbascoe  14677  fiinopn  14699  cnpfval  14890  iscnp3  14898  cnprcl2k  14901  tgcn  14903  lmbr  14908  lmbr2  14909  lmbrf  14910  lmss  14941  cnmptcom  14993  metss  15189  metcnp  15207  metcnpi  15210  metcnpi2  15211  elcncf  15268  cncfi  15273  rescncf  15276  cncfco  15286  cdivcncfap  15299  ellimc3apf  15355  limcdifap  15357  limcmpted  15358  limcimo  15360  limcresi  15361  cnplimclemr  15364  limccoap  15373  dvmptfsum  15420  plycolemc  15453  rpcxpmul2  15608  perfectlem2  15695  lgsquad2lem2  15782  bdbm1.3ii  16363  bj-2inf  16410  bj-omtrans  16428  nninfalllem1  16488  nninfsellemdc  16490  nninfsellemqall  16495