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  vtocl4g  2846  vtocl4ga  2847  eqeu  2947  mo2icl  2956  euind  2964  reu7  2972  reuind  2982  sbctt  3069  sbcnestgf  3149  preq12bg  3819  elint  3896  elintrabg  3903  intab  3919  trss  4158  bm1.3ii  4172  pocl  4357  swopolem  4359  sowlin  4374  frforeq3  4401  frirrg  4404  frind  4406  reusv3  4514  regexmid  4590  ordsoexmid  4617  tfisi  4642  finds2  4656  nnregexmid  4676  vtoclr  4730  2optocl  4759  3optocl  4760  raliunxp  4826  resieq  4977  iss  5013  cnveqb  5146  iotaexab  5258  funmo  5294  fnbrfvb  5631  fvelimab  5647  fvmptssdm  5676  fmptco  5758  fnressn  5782  fressnfv  5783  isoselem  5901  isosolem  5905  ovg  6097  caovcan  6123  caovordig  6124  caovord  6130  f1o2ndf1  6326  poxp  6330  smoeq  6388  smores  6390  tfrlem1  6406  tfrlemi1  6430  tfrexlem  6432  tfri3  6465  oawordriexmid  6568  nnacl  6578  nnmcl  6579  nnacom  6582  nnaass  6583  nndi  6584  nnmass  6585  nnmsucr  6586  nnmcom  6587  nnsucsssuc  6590  nntri3or  6591  nnaordi  6606  nnaword  6609  nnmordi  6614  nnaordex  6626  2ecoptocl  6722  3ecoptocl  6723  th3qlem2  6737  xpdom2g  6941  findcard2  7000  findcard2s  7001  xpfi  7043  supeq1  7102  ordiso2  7151  updjud  7198  nnnninfeq  7244  exmidontriimlem4  7351  exmidontriim  7352  distrnq0  7587  addassnq0  7590  elinp  7602  prcdnql  7612  prcunqu  7613  prarloclem3  7625  caucvgpr  7810  caucvgprpr  7840  ltsosr  7892  caucvgsrlemcau  7921  caucvgsrlemgt1  7923  caucvgsrlemoffres  7928  pitonn  7976  axpre-ltwlin  8011  axcaucvglemres  8027  sup3exmid  9045  nnaddcl  9071  nnmulcl  9072  zaddcllempos  9424  zaddcllemneg  9426  prime  9487  peano5uzti  9496  uzind2  9500  zindd  9506  uzaddcl  9722  exfzdc  10386  infssuzex  10393  nninfdcex  10397  frec2uzltd  10565  frec2uzrdg  10571  frecuzrdgtcl  10574  frecuzrdgg  10578  frecuzrdgfunlem  10581  seq3val  10622  seqvalcd  10623  seq3clss  10633  seq3fveq2  10637  seqfveq2g  10639  seq3shft2  10643  seqshft2g  10644  monoord  10647  seq3split  10650  seqsplitg  10651  seq3caopr3  10653  seqcaopr3g  10654  seq3f1olemp  10677  seqf1oglem2a  10680  seqf1og  10683  seq3id3  10686  seq3id2  10688  seq3homo  10689  seq3z  10690  seqhomog  10692  seqfeq4g  10693  ser3ge0  10698  exp3vallem  10702  expcllem  10712  expap0  10731  mulexp  10740  expadd  10743  expmul  10746  leexp2r  10755  leexp1a  10756  bernneq  10822  modqexp  10828  nn0ltexp2  10871  apexp1  10880  facdiv  10900  faclbnd  10903  faclbnd6  10906  omgadd  10964  seq3coll  11004  wrdind  11193  wrd2ind  11194  shftvalg  11217  shftval4g  11218  cjexp  11274  resqrexlemover  11391  resqrexlemdecn  11393  resqrexlemlo  11394  resqrexlemcalc3  11397  absexp  11460  climshft  11685  climub  11725  climserle  11726  fsum2d  11816  fsumabs  11846  fsumiun  11858  binom  11865  bcxmas  11870  cvgratnnlemnexp  11905  cvgratnnlemmn  11906  clim2prod  11920  prodfap0  11926  prodfrecap  11927  fprodabs  11997  fprod2d  12004  demoivreALT  12155  dvdsfac  12241  bitsinv1  12343  bezoutlemstep  12388  bezoutlemmain  12389  bezoutlemex  12392  dfgcd2  12405  gcdmultiple  12411  rplpwr  12418  nn0seqcvgd  12433  alginv  12439  algcvga  12443  algfx  12444  isprm4  12511  prmind2  12512  prmdvdsexp  12540  prmfac1  12544  eulerthlemrprm  12621  eulerthlema  12622  reumodprminv  12646  pcmpt  12736  pcfac  12743  prmpwdvds  12748  ennnfoneleminc  12852  ennnfonelemkh  12853  ennnfonelemhf1o  12854  ennnfonelemhom  12856  nninfdclemlt  12892  gsumfzz  13397  mulgnnass  13563  mhmmulg  13569  gsumfzconst  13747  srgmulgass  13821  srgpcomp  13822  lmodvsmmulgdi  14155  cnfldexp  14409  gsumfzfsumlemm  14419  mplelbascoe  14524  fiinopn  14546  cnpfval  14737  iscnp3  14745  cnprcl2k  14748  tgcn  14750  lmbr  14755  lmbr2  14756  lmbrf  14757  lmss  14788  cnmptcom  14840  metss  15036  metcnp  15054  metcnpi  15057  metcnpi2  15058  elcncf  15115  cncfi  15120  rescncf  15123  cncfco  15133  cdivcncfap  15146  ellimc3apf  15202  limcdifap  15204  limcmpted  15205  limcimo  15207  limcresi  15208  cnplimclemr  15211  limccoap  15220  dvmptfsum  15267  plycolemc  15300  rpcxpmul2  15455  perfectlem2  15542  lgsquad2lem2  15629  bdbm1.3ii  15961  bj-2inf  16008  bj-omtrans  16026  nninfalllem1  16080  nninfsellemdc  16082  nninfsellemqall  16087