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  893  pm4.14dc  895  imimorbdc  901  pm5.6dc  931  ax11v2  1866  ax11v  1873  equs5or  1876  mo23  2119  nfabdw  2391  2gencl  2833  3gencl  2834  vtocl2gf  2863  vtocl3gf  2864  vtocl4g  2872  vtocl4ga  2873  eqeu  2973  mo2icl  2982  euind  2990  reu7  2998  reuind  3008  sbctt  3095  reu8nf  3110  sbcnestgf  3176  preq12bg  3850  elint  3928  elintrabg  3935  intab  3951  trss  4190  bm1.3ii  4204  pocl  4391  swopolem  4393  sowlin  4408  frforeq3  4435  frirrg  4438  frind  4440  reusv3  4548  regexmid  4624  ordsoexmid  4651  tfisi  4676  finds2  4690  nnregexmid  4710  vtoclr  4764  2optocl  4793  3optocl  4794  raliunxp  4860  resieq  5011  iss  5047  cnveqb  5180  iotaexab  5293  funmo  5329  fnbrfvb  5666  fvelimab  5683  fvmptssdm  5712  fmptco  5794  fnressn  5818  fressnfv  5819  isoselem  5937  isosolem  5941  ovg  6135  caovcan  6161  caovordig  6162  caovord  6168  f1o2ndf1  6364  poxp  6368  smoeq  6426  smores  6428  tfrlem1  6444  tfrlemi1  6468  tfrexlem  6470  tfri3  6503  oawordriexmid  6606  nnacl  6616  nnmcl  6617  nnacom  6620  nnaass  6621  nndi  6622  nnmass  6623  nnmsucr  6624  nnmcom  6625  nnsucsssuc  6628  nntri3or  6629  nnaordi  6644  nnaword  6647  nnmordi  6652  nnaordex  6664  2ecoptocl  6760  3ecoptocl  6761  th3qlem2  6775  xpdom2g  6979  findcard2  7039  findcard2s  7040  xpfi  7082  supeq1  7141  ordiso2  7190  updjud  7237  nnnninfeq  7283  exmidontriimlem4  7394  exmidontriim  7395  distrnq0  7634  addassnq0  7637  elinp  7649  prcdnql  7659  prcunqu  7660  prarloclem3  7672  caucvgpr  7857  caucvgprpr  7887  ltsosr  7939  caucvgsrlemcau  7968  caucvgsrlemgt1  7970  caucvgsrlemoffres  7975  pitonn  8023  axpre-ltwlin  8058  axcaucvglemres  8074  sup3exmid  9092  nnaddcl  9118  nnmulcl  9119  zaddcllempos  9471  zaddcllemneg  9473  prime  9534  peano5uzti  9543  uzind2  9547  zindd  9553  uzaddcl  9769  exfzdc  10433  infssuzex  10440  nninfdcex  10444  frec2uzltd  10612  frec2uzrdg  10618  frecuzrdgtcl  10621  frecuzrdgg  10625  frecuzrdgfunlem  10628  seq3val  10669  seqvalcd  10670  seq3clss  10680  seq3fveq2  10684  seqfveq2g  10686  seq3shft2  10690  seqshft2g  10691  monoord  10694  seq3split  10697  seqsplitg  10698  seq3caopr3  10700  seqcaopr3g  10701  seq3f1olemp  10724  seqf1oglem2a  10727  seqf1og  10730  seq3id3  10733  seq3id2  10735  seq3homo  10736  seq3z  10737  seqhomog  10739  seqfeq4g  10740  ser3ge0  10745  exp3vallem  10749  expcllem  10759  expap0  10778  mulexp  10787  expadd  10790  expmul  10793  leexp2r  10802  leexp1a  10803  bernneq  10869  modqexp  10875  nn0ltexp2  10918  apexp1  10927  facdiv  10947  faclbnd  10950  faclbnd6  10953  omgadd  11011  seq3coll  11051  wrdind  11240  wrd2ind  11241  pfxccatin12lem3  11250  shftvalg  11333  shftval4g  11334  cjexp  11390  resqrexlemover  11507  resqrexlemdecn  11509  resqrexlemlo  11510  resqrexlemcalc3  11513  absexp  11576  climshft  11801  climub  11841  climserle  11842  fsum2d  11932  fsumabs  11962  fsumiun  11974  binom  11981  bcxmas  11986  cvgratnnlemnexp  12021  cvgratnnlemmn  12022  clim2prod  12036  prodfap0  12042  prodfrecap  12043  fprodabs  12113  fprod2d  12120  demoivreALT  12271  dvdsfac  12357  bitsinv1  12459  bezoutlemstep  12504  bezoutlemmain  12505  bezoutlemex  12508  dfgcd2  12521  gcdmultiple  12527  rplpwr  12534  nn0seqcvgd  12549  alginv  12555  algcvga  12559  algfx  12560  isprm4  12627  prmind2  12628  prmdvdsexp  12656  prmfac1  12660  eulerthlemrprm  12737  eulerthlema  12738  reumodprminv  12762  pcmpt  12852  pcfac  12859  prmpwdvds  12864  ennnfoneleminc  12968  ennnfonelemkh  12969  ennnfonelemhf1o  12970  ennnfonelemhom  12972  nninfdclemlt  13008  gsumfzz  13514  mulgnnass  13680  mhmmulg  13686  gsumfzconst  13864  srgmulgass  13938  srgpcomp  13939  lmodvsmmulgdi  14272  cnfldexp  14526  gsumfzfsumlemm  14536  mplelbascoe  14641  fiinopn  14663  cnpfval  14854  iscnp3  14862  cnprcl2k  14865  tgcn  14867  lmbr  14872  lmbr2  14873  lmbrf  14874  lmss  14905  cnmptcom  14957  metss  15153  metcnp  15171  metcnpi  15174  metcnpi2  15175  elcncf  15232  cncfi  15237  rescncf  15240  cncfco  15250  cdivcncfap  15263  ellimc3apf  15319  limcdifap  15321  limcmpted  15322  limcimo  15324  limcresi  15325  cnplimclemr  15328  limccoap  15337  dvmptfsum  15384  plycolemc  15417  rpcxpmul2  15572  perfectlem2  15659  lgsquad2lem2  15746  bdbm1.3ii  16184  bj-2inf  16231  bj-omtrans  16249  nninfalllem1  16305  nninfsellemdc  16307  nninfsellemqall  16312