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  895  pm4.14dc  897  imimorbdc  903  pm5.6dc  933  ax11v2  1868  ax11v  1875  equs5or  1878  mo23  2121  nfabdw  2393  2gencl  2836  3gencl  2837  vtocl2gf  2866  vtocl3gf  2867  vtocl4g  2875  vtocl4ga  2876  eqeu  2976  mo2icl  2985  euind  2993  reu7  3001  reuind  3011  sbctt  3098  reu8nf  3113  sbcnestgf  3179  preq12bg  3856  elint  3934  elintrabg  3941  intab  3957  trss  4196  bm1.3ii  4210  pocl  4400  swopolem  4402  sowlin  4417  frforeq3  4444  frirrg  4447  frind  4449  reusv3  4557  regexmid  4633  ordsoexmid  4660  tfisi  4685  finds2  4699  nnregexmid  4719  vtoclr  4774  2optocl  4803  3optocl  4804  raliunxp  4871  resieq  5023  iss  5059  cnveqb  5192  iotaexab  5305  funmo  5341  fnbrfvb  5684  fvelimab  5702  fvmptssdm  5731  fmptco  5813  fnressn  5840  fressnfv  5841  isoselem  5961  isosolem  5965  ovg  6161  caovcan  6187  caovordig  6188  caovord  6194  f1o2ndf1  6393  poxp  6397  smoeq  6456  smores  6458  tfrlem1  6474  tfrlemi1  6498  tfrexlem  6500  tfri3  6533  oawordriexmid  6638  nnacl  6648  nnmcl  6649  nnacom  6652  nnaass  6653  nndi  6654  nnmass  6655  nnmsucr  6656  nnmcom  6657  nnsucsssuc  6660  nntri3or  6661  nnaordi  6676  nnaword  6679  nnmordi  6684  nnaordex  6696  2ecoptocl  6792  3ecoptocl  6793  th3qlem2  6807  xpdom2g  7016  findcard2  7078  findcard2s  7079  xpfi  7124  supeq1  7185  ordiso2  7234  updjud  7281  nnnninfeq  7327  exmidontriimlem4  7439  exmidontriim  7440  distrnq0  7679  addassnq0  7682  elinp  7694  prcdnql  7704  prcunqu  7705  prarloclem3  7717  caucvgpr  7902  caucvgprpr  7932  ltsosr  7984  caucvgsrlemcau  8013  caucvgsrlemgt1  8015  caucvgsrlemoffres  8020  pitonn  8068  axpre-ltwlin  8103  axcaucvglemres  8119  sup3exmid  9137  nnaddcl  9163  nnmulcl  9164  zaddcllempos  9516  zaddcllemneg  9518  prime  9579  peano5uzti  9588  uzind2  9592  zindd  9598  uzaddcl  9820  exfzdc  10487  infssuzex  10494  nninfdcex  10498  frec2uzltd  10666  frec2uzrdg  10672  frecuzrdgtcl  10675  frecuzrdgg  10679  frecuzrdgfunlem  10682  seq3val  10723  seqvalcd  10724  seq3clss  10734  seq3fveq2  10738  seqfveq2g  10740  seq3shft2  10744  seqshft2g  10745  monoord  10748  seq3split  10751  seqsplitg  10752  seq3caopr3  10754  seqcaopr3g  10755  seq3f1olemp  10778  seqf1oglem2a  10781  seqf1og  10784  seq3id3  10787  seq3id2  10789  seq3homo  10790  seq3z  10791  seqhomog  10793  seqfeq4g  10794  ser3ge0  10799  exp3vallem  10803  expcllem  10813  expap0  10832  mulexp  10841  expadd  10844  expmul  10847  leexp2r  10856  leexp1a  10857  bernneq  10923  modqexp  10929  nn0ltexp2  10972  apexp1  10981  facdiv  11001  faclbnd  11004  faclbnd6  11007  omgadd  11066  seq3coll  11107  wrdind  11307  wrd2ind  11308  pfxccatin12lem3  11317  shftvalg  11401  shftval4g  11402  cjexp  11458  resqrexlemover  11575  resqrexlemdecn  11577  resqrexlemlo  11578  resqrexlemcalc3  11581  absexp  11644  climshft  11869  climub  11909  climserle  11910  fsum2d  12001  fsumabs  12031  fsumiun  12043  binom  12050  bcxmas  12055  cvgratnnlemnexp  12090  cvgratnnlemmn  12091  clim2prod  12105  prodfap0  12111  prodfrecap  12112  fprodabs  12182  fprod2d  12189  demoivreALT  12340  dvdsfac  12426  bitsinv1  12528  bezoutlemstep  12573  bezoutlemmain  12574  bezoutlemex  12577  dfgcd2  12590  gcdmultiple  12596  rplpwr  12603  nn0seqcvgd  12618  alginv  12624  algcvga  12628  algfx  12629  isprm4  12696  prmind2  12697  prmdvdsexp  12725  prmfac1  12729  eulerthlemrprm  12806  eulerthlema  12807  reumodprminv  12831  pcmpt  12921  pcfac  12928  prmpwdvds  12933  ennnfoneleminc  13037  ennnfonelemkh  13038  ennnfonelemhf1o  13039  ennnfonelemhom  13041  nninfdclemlt  13077  gsumfzz  13583  mulgnnass  13749  mhmmulg  13755  gsumfzconst  13933  srgmulgass  14008  srgpcomp  14009  lmodvsmmulgdi  14343  cnfldexp  14597  gsumfzfsumlemm  14607  mplelbascoe  14712  fiinopn  14734  cnpfval  14925  iscnp3  14933  cnprcl2k  14936  tgcn  14938  lmbr  14943  lmbr2  14944  lmbrf  14945  lmss  14976  cnmptcom  15028  metss  15224  metcnp  15242  metcnpi  15245  metcnpi2  15246  elcncf  15303  cncfi  15308  rescncf  15311  cncfco  15321  cdivcncfap  15334  ellimc3apf  15390  limcdifap  15392  limcmpted  15393  limcimo  15395  limcresi  15396  cnplimclemr  15399  limccoap  15408  dvmptfsum  15455  plycolemc  15488  rpcxpmul2  15643  perfectlem2  15730  lgsquad2lem2  15817  eupth2fi  16336  depindlem2  16352  depindlem3  16353  bdbm1.3ii  16512  bj-2inf  16559  bj-omtrans  16577  nninfalllem1  16636  nninfsellemdc  16638  nninfsellemqall  16643