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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  imbi12d  234  imbi2  237  pm5.42  320  imanst  900  pm4.14dc  902  imimorbdc  908  pm5.6dc  938  ax11v2  1873  ax11v  1880  equs5or  1883  mo23  2128  nfabdw  2411  2gencl  2855  3gencl  2856  vtocl2gf  2885  vtocl3gf  2886  vtocl4g  2894  vtocl4ga  2895  eqeu  2996  mo2icl  3005  euind  3013  reu7  3021  reuind  3031  sbctt  3118  reu8nf  3133  sbcnestgf  3199  preq12bg  3898  elint  3976  elintrabg  3983  intab  3999  trss  4240  bm1.3ii  4256  pocl  4450  swopolem  4452  sowlin  4467  frforeq3  4494  frirrg  4497  frind  4499  reusv3  4608  regexmid  4684  ordsoexmid  4711  tfisi  4736  finds2  4750  nnregexmid  4770  vtoclr  4825  2optocl  4854  3optocl  4855  raliunxp  4923  resieq  5075  iss  5112  cnveqb  5246  iotaexab  5359  funmo  5395  fnbrfvb  5744  fvelimab  5762  fvmptssdm  5793  fmptco  5877  fnressn  5904  fressnfv  5905  isoselem  6029  isosolem  6033  ovg  6231  caovcan  6257  caovordig  6258  caovord  6264  f1o2ndf1  6468  poxp  6472  smoeq  6565  smores  6567  tfrlem1  6583  tfrlemi1  6607  tfrexlem  6609  tfri3  6642  oawordriexmid  6747  nnacl  6757  nnmcl  6758  nnacom  6761  nnaass  6762  nndi  6763  nnmass  6764  nnmsucr  6765  nnmcom  6766  nnsucsssuc  6769  nntri3or  6770  nnaordi  6785  nnaword  6788  nnmordi  6793  nnaordex  6805  2ecoptocl  6901  3ecoptocl  6902  th3qlem2  6916  xpdom2g  7135  findcard2  7198  findcard2s  7199  xpfi  7244  supeq1  7333  ordiso2  7382  updjud  7429  nnnninfeq  7475  exmidontriimlem4  7587  exmidontriim  7588  papcotr  7620  distrnq0  7833  addassnq0  7836  elinp  7848  prcdnql  7858  prcunqu  7859  prarloclem3  7871  caucvgpr  8056  caucvgprpr  8086  ltsosr  8138  caucvgsrlemcau  8167  caucvgsrlemgt1  8169  caucvgsrlemoffres  8174  pitonn  8222  axpre-ltwlin  8257  axcaucvglemres  8273  sup3exmid  9296  nnaddcl  9334  nnmulcl  9335  zaddcllempos  9693  zaddcllemneg  9695  prime  9757  peano5uzti  9766  uzind2  9770  zindd  9776  uzaddcl  10003  exfzdc  10677  infssuzex  10684  nninfdcex  10690  frec2uzltd  10862  frec2uzrdg  10868  frecuzrdgtcl  10871  frecuzrdgg  10875  frecuzrdgfunlem  10878  seq3val  10919  seqvalcd  10920  seq3clss  10930  seq3fveq2  10934  seqfveq2g  10936  seq3shft2  10940  seqshft2g  10941  monoord  10944  seq3split  10947  seqsplitg  10948  seq3caopr3  10950  seqcaopr3g  10951  seq3f1olemp  10974  seqf1oglem2a  10977  seqf1og  10980  seq3id3  10983  seq3id2  10985  seq3homo  10986  seq3z  10987  seqhomog  10989  seqfeq4g  10990  ser3ge0  10995  exp3vallem  10999  expcllem  11009  expap0  11028  mulexp  11037  expadd  11040  expmul  11043  leexp2r  11052  leexp1a  11053  bernneq  11120  modqexp  11126  nn0ltexp2  11170  apexp1  11179  facdiv  11199  faclbnd  11202  faclbnd6  11205  omgadd  11265  hashmap  11291  hashf1  11310  seq3coll  11317  wrdind  11517  wrd2ind  11518  pfxccatin12lem3  11527  shftvalg  11624  shftval4g  11625  cjexp  11681  resqrexlemover  11799  resqrexlemdecn  11801  resqrexlemlo  11802  resqrexlemcalc3  11805  absexp  11869  climshft  12096  climub  12136  climserle  12137  fsum2d  12228  fsumabs  12258  fsumiun  12270  binom  12277  bcxmas  12282  cvgratnnlemnexp  12317  cvgratnnlemmn  12318  clim2prod  12332  prodfap0  12338  prodfrecap  12339  fprodabs  12409  fprod2d  12416  demoivreALT  12567  dvdsfac  12653  bitsinv1  12755  bezoutlemstep  12800  bezoutlemmain  12801  bezoutlemex  12804  dfgcd2  12817  gcdmultiple  12823  rplpwr  12830  nn0seqcvgd  12845  alginv  12851  algcvga  12855  algfx  12856  isprm4  12923  prmind2  12924  prmdvdsexp  12953  prmfac1  12957  eulerthlemrprm  13037  eulerthlema  13038  reumodprminv  13062  pcmpt  13152  pcfac  13159  prmpwdvds  13164  prmlem1a  13251  ennnfoneleminc  13361  ennnfonelemkh  13362  ennnfonelemhf1o  13363  ennnfonelemhom  13365  nninfdclemlt  13401  mulgnnass  14020  mhmmulg  14026  gzsumconst  14234  gsumcom2fi  14276  srgmulgass  14401  srgpcomp  14402  lmodvsmmulgdi  14770  cnfldexp  15024  assamulgscm  15153  mplelbascoe  15220  fiinopn  15242  cnpfval  15433  iscnp3  15441  cnprcl2k  15444  tgcn  15446  lmbr  15451  lmbr2  15452  lmbrf  15453  lmss  15484  cnmptcom  15536  metss  15732  metcnp  15750  metcnpi  15753  metcnpi2  15754  elcncf  15811  cncfi  15816  rescncf  15819  cncfco  15829  cdivcncfap  15842  ellimc3apf  15898  limcdifap  15900  limcmpted  15901  limcimo  15903  limcresi  15904  cnplimclemr  15907  limccoap  15916  dvmptfsum  15963  plycolemc  15996  rpcxpmul2  16158  perfectlem2  16312  bcmono  16316  bposlem5  16327  lgsquad2lem2  16418  eupth2fi  16937  depindlem2  16965  depindlem3  16966  bdbm1.3ii  17134  bj-2inf  17181  bj-omtrans  17199  exmidcon  17254  exmidpeirce  17255  wexmiddiffilem  17260  nninfalllem1  17269  nninfsellemdc  17271  nninfsellemqall  17276