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  896  pm4.14dc  898  imimorbdc  904  pm5.6dc  934  ax11v2  1869  ax11v  1876  equs5or  1879  mo23  2122  nfabdw  2403  2gencl  2846  3gencl  2847  vtocl2gf  2876  vtocl3gf  2877  vtocl4g  2885  vtocl4ga  2886  eqeu  2986  mo2icl  2995  euind  3003  reu7  3011  reuind  3021  sbctt  3108  reu8nf  3123  sbcnestgf  3189  preq12bg  3876  elint  3954  elintrabg  3961  intab  3977  trss  4216  bm1.3ii  4230  pocl  4423  swopolem  4425  sowlin  4440  frforeq3  4467  frirrg  4470  frind  4472  reusv3  4580  regexmid  4656  ordsoexmid  4683  tfisi  4708  finds2  4722  nnregexmid  4742  vtoclr  4797  2optocl  4826  3optocl  4827  raliunxp  4895  resieq  5047  iss  5083  cnveqb  5217  iotaexab  5330  funmo  5366  fnbrfvb  5714  fvelimab  5732  fvmptssdm  5761  fmptco  5842  fnressn  5869  fressnfv  5870  isoselem  5992  isosolem  5996  ovg  6192  caovcan  6218  caovordig  6219  caovord  6225  f1o2ndf1  6423  poxp  6427  smoeq  6520  smores  6522  tfrlem1  6538  tfrlemi1  6562  tfrexlem  6564  tfri3  6597  oawordriexmid  6702  nnacl  6712  nnmcl  6713  nnacom  6716  nnaass  6717  nndi  6718  nnmass  6719  nnmsucr  6720  nnmcom  6721  nnsucsssuc  6724  nntri3or  6725  nnaordi  6740  nnaword  6743  nnmordi  6748  nnaordex  6760  2ecoptocl  6856  3ecoptocl  6857  th3qlem2  6871  xpdom2g  7082  findcard2  7145  findcard2s  7146  xpfi  7191  supeq1  7276  ordiso2  7325  updjud  7372  nnnninfeq  7418  exmidontriimlem4  7530  exmidontriim  7531  papcotr  7561  distrnq0  7773  addassnq0  7776  elinp  7788  prcdnql  7798  prcunqu  7799  prarloclem3  7811  caucvgpr  7996  caucvgprpr  8026  ltsosr  8078  caucvgsrlemcau  8107  caucvgsrlemgt1  8109  caucvgsrlemoffres  8114  pitonn  8162  axpre-ltwlin  8197  axcaucvglemres  8213  sup3exmid  9230  nnaddcl  9256  nnmulcl  9257  zaddcllempos  9613  zaddcllemneg  9615  prime  9676  peano5uzti  9685  uzind2  9689  zindd  9695  uzaddcl  9917  exfzdc  10585  infssuzex  10592  nninfdcex  10596  frec2uzltd  10764  frec2uzrdg  10770  frecuzrdgtcl  10773  frecuzrdgg  10777  frecuzrdgfunlem  10780  seq3val  10821  seqvalcd  10822  seq3clss  10832  seq3fveq2  10836  seqfveq2g  10838  seq3shft2  10842  seqshft2g  10843  monoord  10846  seq3split  10849  seqsplitg  10850  seq3caopr3  10852  seqcaopr3g  10853  seq3f1olemp  10876  seqf1oglem2a  10879  seqf1og  10882  seq3id3  10885  seq3id2  10887  seq3homo  10888  seq3z  10889  seqhomog  10891  seqfeq4g  10892  ser3ge0  10897  exp3vallem  10901  expcllem  10911  expap0  10930  mulexp  10939  expadd  10942  expmul  10945  leexp2r  10954  leexp1a  10955  bernneq  11021  modqexp  11027  nn0ltexp2  11070  apexp1  11079  facdiv  11099  faclbnd  11102  faclbnd6  11105  omgadd  11164  seq3coll  11210  wrdind  11410  wrd2ind  11411  pfxccatin12lem3  11420  shftvalg  11517  shftval4g  11518  cjexp  11574  resqrexlemover  11691  resqrexlemdecn  11693  resqrexlemlo  11694  resqrexlemcalc3  11697  absexp  11760  climshft  11985  climub  12025  climserle  12026  fsum2d  12117  fsumabs  12147  fsumiun  12159  binom  12166  bcxmas  12171  cvgratnnlemnexp  12206  cvgratnnlemmn  12207  clim2prod  12221  prodfap0  12227  prodfrecap  12228  fprodabs  12298  fprod2d  12305  demoivreALT  12456  dvdsfac  12542  bitsinv1  12644  bezoutlemstep  12689  bezoutlemmain  12690  bezoutlemex  12693  dfgcd2  12706  gcdmultiple  12712  rplpwr  12719  nn0seqcvgd  12734  alginv  12740  algcvga  12744  algfx  12745  isprm4  12812  prmind2  12813  prmdvdsexp  12841  prmfac1  12845  eulerthlemrprm  12922  eulerthlema  12923  reumodprminv  12947  pcmpt  13037  pcfac  13044  prmpwdvds  13049  ennnfoneleminc  13154  ennnfonelemkh  13155  ennnfonelemhf1o  13156  ennnfonelemhom  13158  nninfdclemlt  13194  gsumfzz  13700  mulgnnass  13866  mhmmulg  13872  gsumfzconst  14050  srgmulgass  14125  srgpcomp  14126  lmodvsmmulgdi  14463  cnfldexp  14717  gsumfzfsumlemm  14727  mplelbascoe  14839  fiinopn  14861  cnpfval  15052  iscnp3  15060  cnprcl2k  15063  tgcn  15065  lmbr  15070  lmbr2  15071  lmbrf  15072  lmss  15103  cnmptcom  15155  metss  15351  metcnp  15369  metcnpi  15372  metcnpi2  15373  elcncf  15430  cncfi  15435  rescncf  15438  cncfco  15448  cdivcncfap  15461  ellimc3apf  15517  limcdifap  15519  limcmpted  15520  limcimo  15522  limcresi  15523  cnplimclemr  15526  limccoap  15535  dvmptfsum  15582  plycolemc  15615  rpcxpmul2  15770  perfectlem2  15860  lgsquad2lem2  15947  eupth2fi  16466  depindlem2  16494  depindlem3  16495  bdbm1.3ii  16653  bj-2inf  16700  bj-omtrans  16718  exmidcon  16772  exmidpeirce  16773  nninfalllem1  16778  nninfsellemdc  16780  nninfsellemqall  16785