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  1793  ax11v  1800  equs5or  1803  mo23  2041  2gencl  2722  3gencl  2723  vtocl2gf  2751  vtocl3gf  2752  eqeu  2858  mo2icl  2867  euind  2875  reu7  2883  reuind  2893  sbctt  2979  sbcnestgf  3056  preq12bg  3708  elint  3785  elintrabg  3792  intab  3808  trss  4043  bm1.3ii  4057  pocl  4233  swopolem  4235  sowlin  4250  frforeq3  4277  frirrg  4280  frind  4282  reusv3  4389  regexmid  4458  ordsoexmid  4485  tfisi  4509  finds2  4523  nnregexmid  4542  vtoclr  4595  2optocl  4624  3optocl  4625  raliunxp  4688  resieq  4837  iss  4873  cnveqb  5002  funmo  5146  fnbrfvb  5470  fvelimab  5485  fvmptssdm  5513  fmptco  5594  fnressn  5614  fressnfv  5615  isoselem  5729  isosolem  5733  ovg  5917  caovcan  5943  caovordig  5944  caovord  5950  f1o2ndf1  6133  poxp  6137  smoeq  6195  smores  6197  tfrlem1  6213  tfrlemi1  6237  tfrexlem  6239  tfri3  6272  oawordriexmid  6374  nnacl  6384  nnmcl  6385  nnacom  6388  nnaass  6389  nndi  6390  nnmass  6391  nnmsucr  6392  nnmcom  6393  nnsucsssuc  6396  nntri3or  6397  nnaordi  6412  nnaword  6415  nnmordi  6420  nnaordex  6431  2ecoptocl  6525  3ecoptocl  6526  th3qlem2  6540  xpdom2g  6734  findcard2  6791  findcard2s  6792  xpfi  6826  supeq1  6881  ordiso2  6928  updjud  6975  distrnq0  7291  addassnq0  7294  elinp  7306  prcdnql  7316  prcunqu  7317  prarloclem3  7329  caucvgpr  7514  caucvgprpr  7544  ltsosr  7596  caucvgsrlemcau  7625  caucvgsrlemgt1  7627  caucvgsrlemoffres  7632  pitonn  7680  axpre-ltwlin  7715  axcaucvglemres  7731  sup3exmid  8739  nnaddcl  8764  nnmulcl  8765  zaddcllempos  9115  zaddcllemneg  9117  prime  9174  peano5uzti  9183  uzind2  9187  zindd  9193  uzaddcl  9408  exfzdc  10048  frec2uzltd  10207  frec2uzrdg  10213  frecuzrdgtcl  10216  frecuzrdgg  10220  frecuzrdgfunlem  10223  seq3val  10262  seqvalcd  10263  seq3clss  10271  seq3fveq2  10273  seq3shft2  10277  monoord  10280  seq3split  10283  seq3caopr3  10285  seq3f1olemp  10306  seq3id3  10311  seq3id2  10313  seq3homo  10314  seq3z  10315  ser3ge0  10321  exp3vallem  10325  expcllem  10335  expap0  10354  mulexp  10363  expadd  10366  expmul  10369  leexp2r  10378  leexp1a  10379  bernneq  10443  apexp1  10496  facdiv  10516  faclbnd  10519  faclbnd6  10522  omgadd  10580  seq3coll  10617  shftvalg  10640  shftval4g  10641  cjexp  10697  resqrexlemover  10814  resqrexlemdecn  10816  resqrexlemlo  10817  resqrexlemcalc3  10820  absexp  10883  climshft  11105  climub  11145  climserle  11146  fsum2d  11236  fsumabs  11266  fsumiun  11278  binom  11285  bcxmas  11290  cvgratnnlemnexp  11325  cvgratnnlemmn  11326  clim2prod  11340  prodfap0  11346  prodfrecap  11347  demoivreALT  11516  dvdsfac  11594  infssuzex  11678  bezoutlemstep  11721  bezoutlemmain  11722  bezoutlemex  11725  dfgcd2  11738  gcdmultiple  11744  rplpwr  11751  nn0seqcvgd  11758  alginv  11764  algcvga  11768  algfx  11769  isprm4  11836  prmind2  11837  prmdvdsexp  11862  prmfac1  11866  ennnfoneleminc  11960  ennnfonelemkh  11961  ennnfonelemhf1o  11962  ennnfonelemhom  11964  fiinopn  12210  cnpfval  12403  iscnp3  12411  cnprcl2k  12414  tgcn  12416  lmbr  12421  lmbr2  12422  lmbrf  12423  lmss  12454  cnmptcom  12506  metss  12702  metcnp  12720  metcnpi  12723  metcnpi2  12724  elcncf  12768  cncfi  12773  rescncf  12776  cncfco  12786  cdivcncfap  12795  ellimc3apf  12837  limcdifap  12839  limcmpted  12840  limcimo  12842  limcresi  12843  cnplimclemr  12846  limccoap  12855  bdbm1.3ii  13260  bj-2inf  13307  bj-omtrans  13325  nninfalllemn  13377  nninfalllem1  13378  nninfsellemdc  13381  nninfsellemqall  13386