Theorem imbi2d 229

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 181	1 ⊢ (𝜑 → ((𝜃 → 𝜓) ↔ (𝜃 → 𝜒)))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  imbi12d  233  imbi2  236  pm5.42  318  imanst  874  pm4.14dc  876  imimorbdc  882  pm5.6dc  912  ax11v2  1800  ax11v  1807  equs5or  1810  mo23  2047  nfabdw  2318  2gencl  2745  3gencl  2746  vtocl2gf  2774  vtocl3gf  2775  eqeu  2882  mo2icl  2891  euind  2899  reu7  2907  reuind  2917  sbctt  3003  sbcnestgf  3082  preq12bg  3736  elint  3813  elintrabg  3820  intab  3836  trss  4071  bm1.3ii  4085  pocl  4263  swopolem  4265  sowlin  4280  frforeq3  4307  frirrg  4310  frind  4312  reusv3  4419  regexmid  4493  ordsoexmid  4520  tfisi  4545  finds2  4559  nnregexmid  4579  vtoclr  4633  2optocl  4662  3optocl  4663  raliunxp  4726  resieq  4875  iss  4911  cnveqb  5040  funmo  5184  fnbrfvb  5508  fvelimab  5523  fvmptssdm  5551  fmptco  5632  fnressn  5652  fressnfv  5653  isoselem  5767  isosolem  5771  ovg  5956  caovcan  5982  caovordig  5983  caovord  5989  f1o2ndf1  6172  poxp  6176  smoeq  6234  smores  6236  tfrlem1  6252  tfrlemi1  6276  tfrexlem  6278  tfri3  6311  oawordriexmid  6414  nnacl  6424  nnmcl  6425  nnacom  6428  nnaass  6429  nndi  6430  nnmass  6431  nnmsucr  6432  nnmcom  6433  nnsucsssuc  6436  nntri3or  6437  nnaordi  6452  nnaword  6455  nnmordi  6460  nnaordex  6471  2ecoptocl  6565  3ecoptocl  6566  th3qlem2  6580  xpdom2g  6774  findcard2  6831  findcard2s  6832  xpfi  6871  supeq1  6927  ordiso2  6974  updjud  7021  nnnninfeq  7066  exmidontriimlem4  7154  exmidontriim  7155  distrnq0  7374  addassnq0  7377  elinp  7389  prcdnql  7399  prcunqu  7400  prarloclem3  7412  caucvgpr  7597  caucvgprpr  7627  ltsosr  7679  caucvgsrlemcau  7708  caucvgsrlemgt1  7710  caucvgsrlemoffres  7715  pitonn  7763  axpre-ltwlin  7798  axcaucvglemres  7814  sup3exmid  8823  nnaddcl  8848  nnmulcl  8849  zaddcllempos  9199  zaddcllemneg  9201  prime  9258  peano5uzti  9267  uzind2  9271  zindd  9277  uzaddcl  9492  exfzdc  10134  frec2uzltd  10297  frec2uzrdg  10303  frecuzrdgtcl  10306  frecuzrdgg  10310  frecuzrdgfunlem  10313  seq3val  10352  seqvalcd  10353  seq3clss  10361  seq3fveq2  10363  seq3shft2  10367  monoord  10370  seq3split  10373  seq3caopr3  10375  seq3f1olemp  10396  seq3id3  10401  seq3id2  10403  seq3homo  10404  seq3z  10405  ser3ge0  10411  exp3vallem  10415  expcllem  10425  expap0  10444  mulexp  10453  expadd  10456  expmul  10459  leexp2r  10468  leexp1a  10469  bernneq  10533  modqexp  10539  apexp1  10587  facdiv  10607  faclbnd  10610  faclbnd6  10613  omgadd  10671  seq3coll  10708  shftvalg  10731  shftval4g  10732  cjexp  10788  resqrexlemover  10905  resqrexlemdecn  10907  resqrexlemlo  10908  resqrexlemcalc3  10911  absexp  10974  climshft  11196  climub  11236  climserle  11237  fsum2d  11327  fsumabs  11357  fsumiun  11369  binom  11376  bcxmas  11381  cvgratnnlemnexp  11416  cvgratnnlemmn  11417  clim2prod  11431  prodfap0  11437  prodfrecap  11438  fprodabs  11508  fprod2d  11515  demoivreALT  11665  dvdsfac  11746  infssuzex  11830  nninfdcex  11833  bezoutlemstep  11875  bezoutlemmain  11876  bezoutlemex  11879  dfgcd2  11892  gcdmultiple  11898  rplpwr  11905  nn0seqcvgd  11912  alginv  11918  algcvga  11922  algfx  11923  isprm4  11990  prmind2  11991  prmdvdsexp  12017  prmfac1  12021  eulerthlemrprm  12096  eulerthlema  12097  ennnfoneleminc  12127  ennnfonelemkh  12128  ennnfonelemhf1o  12129  ennnfonelemhom  12131  nninfdclemlt  12169  fiinopn  12389  cnpfval  12582  iscnp3  12590  cnprcl2k  12593  tgcn  12595  lmbr  12600  lmbr2  12601  lmbrf  12602  lmss  12633  cnmptcom  12685  metss  12881  metcnp  12899  metcnpi  12902  metcnpi2  12903  elcncf  12947  cncfi  12952  rescncf  12955  cncfco  12965  cdivcncfap  12974  ellimc3apf  13016  limcdifap  13018  limcmpted  13019  limcimo  13021  limcresi  13022  cnplimclemr  13025  limccoap  13034  bdbm1.3ii  13453  bj-2inf  13500  bj-omtrans  13518  nninfalllem1  13567  nninfsellemdc  13569  nninfsellemqall  13574