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  890  pm4.14dc  892  imimorbdc  898  pm5.6dc  928  ax11v2  1844  ax11v  1851  equs5or  1854  mo23  2096  nfabdw  2368  2gencl  2807  3gencl  2808  vtocl2gf  2837  vtocl3gf  2838  eqeu  2945  mo2icl  2954  euind  2962  reu7  2970  reuind  2980  sbctt  3067  sbcnestgf  3147  preq12bg  3817  elint  3894  elintrabg  3901  intab  3917  trss  4156  bm1.3ii  4170  pocl  4355  swopolem  4357  sowlin  4372  frforeq3  4399  frirrg  4402  frind  4404  reusv3  4512  regexmid  4588  ordsoexmid  4615  tfisi  4640  finds2  4654  nnregexmid  4674  vtoclr  4728  2optocl  4757  3optocl  4758  raliunxp  4824  resieq  4975  iss  5011  cnveqb  5144  iotaexab  5256  funmo  5292  fnbrfvb  5629  fvelimab  5645  fvmptssdm  5674  fmptco  5756  fnressn  5780  fressnfv  5781  isoselem  5899  isosolem  5903  ovg  6095  caovcan  6121  caovordig  6122  caovord  6128  f1o2ndf1  6324  poxp  6328  smoeq  6386  smores  6388  tfrlem1  6404  tfrlemi1  6428  tfrexlem  6430  tfri3  6463  oawordriexmid  6566  nnacl  6576  nnmcl  6577  nnacom  6580  nnaass  6581  nndi  6582  nnmass  6583  nnmsucr  6584  nnmcom  6585  nnsucsssuc  6588  nntri3or  6589  nnaordi  6604  nnaword  6607  nnmordi  6612  nnaordex  6624  2ecoptocl  6720  3ecoptocl  6721  th3qlem2  6735  xpdom2g  6939  findcard2  6998  findcard2s  6999  xpfi  7041  supeq1  7100  ordiso2  7149  updjud  7196  nnnninfeq  7242  exmidontriimlem4  7349  exmidontriim  7350  distrnq0  7585  addassnq0  7588  elinp  7600  prcdnql  7610  prcunqu  7611  prarloclem3  7623  caucvgpr  7808  caucvgprpr  7838  ltsosr  7890  caucvgsrlemcau  7919  caucvgsrlemgt1  7921  caucvgsrlemoffres  7926  pitonn  7974  axpre-ltwlin  8009  axcaucvglemres  8025  sup3exmid  9043  nnaddcl  9069  nnmulcl  9070  zaddcllempos  9422  zaddcllemneg  9424  prime  9485  peano5uzti  9494  uzind2  9498  zindd  9504  uzaddcl  9720  exfzdc  10382  infssuzex  10389  nninfdcex  10393  frec2uzltd  10561  frec2uzrdg  10567  frecuzrdgtcl  10570  frecuzrdgg  10574  frecuzrdgfunlem  10577  seq3val  10618  seqvalcd  10619  seq3clss  10629  seq3fveq2  10633  seqfveq2g  10635  seq3shft2  10639  seqshft2g  10640  monoord  10643  seq3split  10646  seqsplitg  10647  seq3caopr3  10649  seqcaopr3g  10650  seq3f1olemp  10673  seqf1oglem2a  10676  seqf1og  10679  seq3id3  10682  seq3id2  10684  seq3homo  10685  seq3z  10686  seqhomog  10688  seqfeq4g  10689  ser3ge0  10694  exp3vallem  10698  expcllem  10708  expap0  10727  mulexp  10736  expadd  10739  expmul  10742  leexp2r  10751  leexp1a  10752  bernneq  10818  modqexp  10824  nn0ltexp2  10867  apexp1  10876  facdiv  10896  faclbnd  10899  faclbnd6  10902  omgadd  10960  seq3coll  11000  shftvalg  11197  shftval4g  11198  cjexp  11254  resqrexlemover  11371  resqrexlemdecn  11373  resqrexlemlo  11374  resqrexlemcalc3  11377  absexp  11440  climshft  11665  climub  11705  climserle  11706  fsum2d  11796  fsumabs  11826  fsumiun  11838  binom  11845  bcxmas  11850  cvgratnnlemnexp  11885  cvgratnnlemmn  11886  clim2prod  11900  prodfap0  11906  prodfrecap  11907  fprodabs  11977  fprod2d  11984  demoivreALT  12135  dvdsfac  12221  bitsinv1  12323  bezoutlemstep  12368  bezoutlemmain  12369  bezoutlemex  12372  dfgcd2  12385  gcdmultiple  12391  rplpwr  12398  nn0seqcvgd  12413  alginv  12419  algcvga  12423  algfx  12424  isprm4  12491  prmind2  12492  prmdvdsexp  12520  prmfac1  12524  eulerthlemrprm  12601  eulerthlema  12602  reumodprminv  12626  pcmpt  12716  pcfac  12723  prmpwdvds  12728  ennnfoneleminc  12832  ennnfonelemkh  12833  ennnfonelemhf1o  12834  ennnfonelemhom  12836  nninfdclemlt  12872  gsumfzz  13377  mulgnnass  13543  mhmmulg  13549  gsumfzconst  13727  srgmulgass  13801  srgpcomp  13802  lmodvsmmulgdi  14135  cnfldexp  14389  gsumfzfsumlemm  14399  mplelbascoe  14504  fiinopn  14526  cnpfval  14717  iscnp3  14725  cnprcl2k  14728  tgcn  14730  lmbr  14735  lmbr2  14736  lmbrf  14737  lmss  14768  cnmptcom  14820  metss  15016  metcnp  15034  metcnpi  15037  metcnpi2  15038  elcncf  15095  cncfi  15100  rescncf  15103  cncfco  15113  cdivcncfap  15126  ellimc3apf  15182  limcdifap  15184  limcmpted  15185  limcimo  15187  limcresi  15188  cnplimclemr  15191  limccoap  15200  dvmptfsum  15247  plycolemc  15280  rpcxpmul2  15435  perfectlem2  15522  lgsquad2lem2  15609  bdbm1.3ii  15941  bj-2inf  15988  bj-omtrans  16006  nninfalllem1  16060  nninfsellemdc  16062  nninfsellemqall  16067