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  1831  ax11v  1838  equs5or  1841  mo23  2083  nfabdw  2355  2gencl  2793  3gencl  2794  vtocl2gf  2822  vtocl3gf  2823  eqeu  2930  mo2icl  2939  euind  2947  reu7  2955  reuind  2965  sbctt  3052  sbcnestgf  3132  preq12bg  3799  elint  3876  elintrabg  3883  intab  3899  trss  4136  bm1.3ii  4150  pocl  4334  swopolem  4336  sowlin  4351  frforeq3  4378  frirrg  4381  frind  4383  reusv3  4491  regexmid  4567  ordsoexmid  4594  tfisi  4619  finds2  4633  nnregexmid  4653  vtoclr  4707  2optocl  4736  3optocl  4737  raliunxp  4803  resieq  4952  iss  4988  cnveqb  5121  iotaexab  5233  funmo  5269  fnbrfvb  5597  fvelimab  5613  fvmptssdm  5642  fmptco  5724  fnressn  5744  fressnfv  5745  isoselem  5863  isosolem  5867  ovg  6057  caovcan  6083  caovordig  6084  caovord  6090  f1o2ndf1  6281  poxp  6285  smoeq  6343  smores  6345  tfrlem1  6361  tfrlemi1  6385  tfrexlem  6387  tfri3  6420  oawordriexmid  6523  nnacl  6533  nnmcl  6534  nnacom  6537  nnaass  6538  nndi  6539  nnmass  6540  nnmsucr  6541  nnmcom  6542  nnsucsssuc  6545  nntri3or  6546  nnaordi  6561  nnaword  6564  nnmordi  6569  nnaordex  6581  2ecoptocl  6677  3ecoptocl  6678  th3qlem2  6692  xpdom2g  6886  findcard2  6945  findcard2s  6946  xpfi  6986  supeq1  7045  ordiso2  7094  updjud  7141  nnnninfeq  7187  exmidontriimlem4  7284  exmidontriim  7285  distrnq0  7519  addassnq0  7522  elinp  7534  prcdnql  7544  prcunqu  7545  prarloclem3  7557  caucvgpr  7742  caucvgprpr  7772  ltsosr  7824  caucvgsrlemcau  7853  caucvgsrlemgt1  7855  caucvgsrlemoffres  7860  pitonn  7908  axpre-ltwlin  7943  axcaucvglemres  7959  sup3exmid  8976  nnaddcl  9002  nnmulcl  9003  zaddcllempos  9354  zaddcllemneg  9356  prime  9416  peano5uzti  9425  uzind2  9429  zindd  9435  uzaddcl  9651  exfzdc  10307  frec2uzltd  10474  frec2uzrdg  10480  frecuzrdgtcl  10483  frecuzrdgg  10487  frecuzrdgfunlem  10490  seq3val  10531  seqvalcd  10532  seq3clss  10542  seq3fveq2  10546  seqfveq2g  10548  seq3shft2  10552  seqshft2g  10553  monoord  10556  seq3split  10559  seqsplitg  10560  seq3caopr3  10562  seqcaopr3g  10563  seq3f1olemp  10586  seqf1oglem2a  10589  seqf1og  10592  seq3id3  10595  seq3id2  10597  seq3homo  10598  seq3z  10599  seqhomog  10601  seqfeq4g  10602  ser3ge0  10607  exp3vallem  10611  expcllem  10621  expap0  10640  mulexp  10649  expadd  10652  expmul  10655  leexp2r  10664  leexp1a  10665  bernneq  10731  modqexp  10737  nn0ltexp2  10780  apexp1  10789  facdiv  10809  faclbnd  10812  faclbnd6  10815  omgadd  10873  seq3coll  10913  shftvalg  10980  shftval4g  10981  cjexp  11037  resqrexlemover  11154  resqrexlemdecn  11156  resqrexlemlo  11157  resqrexlemcalc3  11160  absexp  11223  climshft  11447  climub  11487  climserle  11488  fsum2d  11578  fsumabs  11608  fsumiun  11620  binom  11627  bcxmas  11632  cvgratnnlemnexp  11667  cvgratnnlemmn  11668  clim2prod  11682  prodfap0  11688  prodfrecap  11689  fprodabs  11759  fprod2d  11766  demoivreALT  11917  dvdsfac  12002  infssuzex  12086  nninfdcex  12090  bezoutlemstep  12134  bezoutlemmain  12135  bezoutlemex  12138  dfgcd2  12151  gcdmultiple  12157  rplpwr  12164  nn0seqcvgd  12179  alginv  12185  algcvga  12189  algfx  12190  isprm4  12257  prmind2  12258  prmdvdsexp  12286  prmfac1  12290  eulerthlemrprm  12367  eulerthlema  12368  reumodprminv  12391  pcmpt  12481  pcfac  12488  prmpwdvds  12493  ennnfoneleminc  12568  ennnfonelemkh  12569  ennnfonelemhf1o  12570  ennnfonelemhom  12572  nninfdclemlt  12608  gsumfzz  13067  mulgnnass  13227  mhmmulg  13233  gsumfzconst  13411  srgmulgass  13485  srgpcomp  13486  lmodvsmmulgdi  13819  cnfldexp  14065  gsumfzfsumlemm  14075  fiinopn  14172  cnpfval  14363  iscnp3  14371  cnprcl2k  14374  tgcn  14376  lmbr  14381  lmbr2  14382  lmbrf  14383  lmss  14414  cnmptcom  14466  metss  14662  metcnp  14680  metcnpi  14683  metcnpi2  14684  elcncf  14728  cncfi  14733  rescncf  14736  cncfco  14746  cdivcncfap  14758  ellimc3apf  14814  limcdifap  14816  limcmpted  14817  limcimo  14819  limcresi  14820  cnplimclemr  14823  limccoap  14832  bdbm1.3ii  15383  bj-2inf  15430  bj-omtrans  15448  nninfalllem1  15498  nninfsellemdc  15500  nninfsellemqall  15505