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  3854  elint  3932  elintrabg  3939  intab  3955  trss  4194  bm1.3ii  4208  pocl  4398  swopolem  4400  sowlin  4415  frforeq3  4442  frirrg  4445  frind  4447  reusv3  4555  regexmid  4631  ordsoexmid  4658  tfisi  4683  finds2  4697  nnregexmid  4717  vtoclr  4772  2optocl  4801  3optocl  4802  raliunxp  4869  resieq  5021  iss  5057  cnveqb  5190  iotaexab  5303  funmo  5339  fnbrfvb  5680  fvelimab  5698  fvmptssdm  5727  fmptco  5809  fnressn  5835  fressnfv  5836  isoselem  5956  isosolem  5960  ovg  6156  caovcan  6182  caovordig  6183  caovord  6189  f1o2ndf1  6388  poxp  6392  smoeq  6451  smores  6453  tfrlem1  6469  tfrlemi1  6493  tfrexlem  6495  tfri3  6528  oawordriexmid  6633  nnacl  6643  nnmcl  6644  nnacom  6647  nnaass  6648  nndi  6649  nnmass  6650  nnmsucr  6651  nnmcom  6652  nnsucsssuc  6655  nntri3or  6656  nnaordi  6671  nnaword  6674  nnmordi  6679  nnaordex  6691  2ecoptocl  6787  3ecoptocl  6788  th3qlem2  6802  xpdom2g  7011  findcard2  7073  findcard2s  7074  xpfi  7119  supeq1  7179  ordiso2  7228  updjud  7275  nnnninfeq  7321  exmidontriimlem4  7432  exmidontriim  7433  distrnq0  7672  addassnq0  7675  elinp  7687  prcdnql  7697  prcunqu  7698  prarloclem3  7710  caucvgpr  7895  caucvgprpr  7925  ltsosr  7977  caucvgsrlemcau  8006  caucvgsrlemgt1  8008  caucvgsrlemoffres  8013  pitonn  8061  axpre-ltwlin  8096  axcaucvglemres  8112  sup3exmid  9130  nnaddcl  9156  nnmulcl  9157  zaddcllempos  9509  zaddcllemneg  9511  prime  9572  peano5uzti  9581  uzind2  9585  zindd  9591  uzaddcl  9813  exfzdc  10479  infssuzex  10486  nninfdcex  10490  frec2uzltd  10658  frec2uzrdg  10664  frecuzrdgtcl  10667  frecuzrdgg  10671  frecuzrdgfunlem  10674  seq3val  10715  seqvalcd  10716  seq3clss  10726  seq3fveq2  10730  seqfveq2g  10732  seq3shft2  10736  seqshft2g  10737  monoord  10740  seq3split  10743  seqsplitg  10744  seq3caopr3  10746  seqcaopr3g  10747  seq3f1olemp  10770  seqf1oglem2a  10773  seqf1og  10776  seq3id3  10779  seq3id2  10781  seq3homo  10782  seq3z  10783  seqhomog  10785  seqfeq4g  10786  ser3ge0  10791  exp3vallem  10795  expcllem  10805  expap0  10824  mulexp  10833  expadd  10836  expmul  10839  leexp2r  10848  leexp1a  10849  bernneq  10915  modqexp  10921  nn0ltexp2  10964  apexp1  10973  facdiv  10993  faclbnd  10996  faclbnd6  10999  omgadd  11058  seq3coll  11099  wrdind  11296  wrd2ind  11297  pfxccatin12lem3  11306  shftvalg  11390  shftval4g  11391  cjexp  11447  resqrexlemover  11564  resqrexlemdecn  11566  resqrexlemlo  11567  resqrexlemcalc3  11570  absexp  11633  climshft  11858  climub  11898  climserle  11899  fsum2d  11989  fsumabs  12019  fsumiun  12031  binom  12038  bcxmas  12043  cvgratnnlemnexp  12078  cvgratnnlemmn  12079  clim2prod  12093  prodfap0  12099  prodfrecap  12100  fprodabs  12170  fprod2d  12177  demoivreALT  12328  dvdsfac  12414  bitsinv1  12516  bezoutlemstep  12561  bezoutlemmain  12562  bezoutlemex  12565  dfgcd2  12578  gcdmultiple  12584  rplpwr  12591  nn0seqcvgd  12606  alginv  12612  algcvga  12616  algfx  12617  isprm4  12684  prmind2  12685  prmdvdsexp  12713  prmfac1  12717  eulerthlemrprm  12794  eulerthlema  12795  reumodprminv  12819  pcmpt  12909  pcfac  12916  prmpwdvds  12921  ennnfoneleminc  13025  ennnfonelemkh  13026  ennnfonelemhf1o  13027  ennnfonelemhom  13029  nninfdclemlt  13065  gsumfzz  13571  mulgnnass  13737  mhmmulg  13743  gsumfzconst  13921  srgmulgass  13995  srgpcomp  13996  lmodvsmmulgdi  14330  cnfldexp  14584  gsumfzfsumlemm  14594  mplelbascoe  14699  fiinopn  14721  cnpfval  14912  iscnp3  14920  cnprcl2k  14923  tgcn  14925  lmbr  14930  lmbr2  14931  lmbrf  14932  lmss  14963  cnmptcom  15015  metss  15211  metcnp  15229  metcnpi  15232  metcnpi2  15233  elcncf  15290  cncfi  15295  rescncf  15298  cncfco  15308  cdivcncfap  15321  ellimc3apf  15377  limcdifap  15379  limcmpted  15380  limcimo  15382  limcresi  15383  cnplimclemr  15386  limccoap  15395  dvmptfsum  15442  plycolemc  15475  rpcxpmul2  15630  perfectlem2  15717  lgsquad2lem2  15804  bdbm1.3ii  16436  bj-2inf  16483  bj-omtrans  16501  nninfalllem1  16560  nninfsellemdc  16562  nninfsellemqall  16567