Theorem anbi2d 437

Description: Deduction adding a left conjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)

Hypothesis

Ref	Expression
anbid.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
anbi2d	⊢ (𝜑 → ((𝜃 ∧ 𝜓) ↔ (𝜃 ∧ 𝜒)))

Proof of Theorem anbi2d

Step	Hyp	Ref	Expression
1		anbid.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	a1d 22	. 2 ⊢ (𝜑 → (𝜃 → (𝜓 ↔ 𝜒)))
3	2	pm5.32d 423	1 ⊢ (𝜑 → ((𝜃 ∧ 𝜓) ↔ (𝜃 ∧ 𝜒)))

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  anbi2  440  anbi12d  442  bi2anan9  538  dn1dc  867  xorbi2d  1271  dfbi3dc  1288  xordidc  1290  eleq2  2101  ceqsex2  2594  ceqsex6v  2598  vtocl2gaf  2620  ceqsrex2v  2676  mob2  2721  eqreu  2733  nelrdva  2746  psssstr  3051  undif4  3284  r19.27m  3316  ifbi  3348  preq12bg  3544  opeq2  3550  ralunsn  3568  intab  3644  opabbid  3822  opthg  3975  pocl  4040  ordelord  4118  ordtriexmid  4247  ontr2exmid  4250  onsucsssucexmid  4252  tfisi  4310  xpeq2  4360  rabxp  4380  vtoclr  4388  opeliunxp  4395  posng  4412  opbrop  4419  rexiunxp  4478  elrnmpt1  4585  dfres2  4658  brcodir  4712  poltletr  4725  xp11m  4759  elxp4  4808  elxp5  4809  dffun4f  4918  fununi  4967  fneq2  4988  fnun  5005  feq3  5032  foeq3  5104  funfveu  5188  funbrfv  5212  ssimaexg  5235  fvopab3g  5245  fvopab3ig  5246  fvelrn  5298  fmptco  5330  fsn2  5337  elunirn  5405  isoeq2  5442  isoeq3  5443  isocnv2  5452  isoini  5457  isopolem  5461  f1oiso  5465  f1oiso2  5466  oprabbid  5558  cbvoprab3  5580  mpt2mptx  5595  mpt2fun  5603  ov  5620  ovi3  5637  ov6g  5638  ovg  5639  caoftrn  5736  f1o2ndf1  5849  xporderlem  5852  brtpos2  5866  brtposg  5869  dftpos4  5878  recseq  5921  tfrlem3-2  5927  tfrlem3-2d  5928  tfrlemi1  5946  tfrexlem  5948  freceq1  5979  freceq2  5980  frecsuc  5991  nnaordex  6100  brecop  6196  eroveu  6197  erovlem  6198  ecopovtrn  6203  ecopovtrng  6206  th3qlem1  6208  th3qlem2  6209  th3q  6211  domeng  6233  dom2lem  6252  xpcomco  6300  xpassen  6304  xpdom2  6305  phplem3g  6319  ssfiexmid  6336  findcard2  6346  findcard2s  6347  findcard2d  6348  findcard2sd  6349  diffifi  6351  recexnq  6488  recmulnqg  6489  ltsonq  6496  enq0sym  6530  enq0ref  6531  enq0tr  6532  enq0breq  6534  addnq0mo  6545  mulnq0mo  6546  addnnnq0  6547  mulnnnq0  6548  elinp  6572  prdisj  6590  prarloclem3  6595  prarloc  6601  distrlem5prl  6684  distrlem5pru  6685  ltexprlemell  6696  ltexprlemelu  6697  recexprlemm  6722  addsrmo  6828  mulsrmo  6829  addsrpr  6830  mulsrpr  6831  lttrsr  6847  recexgt0sr  6858  mulgt0sr  6862  ltresr  6915  axprecex  6954  axpre-lttrn  6958  axpre-mulgt0  6961  lesub0  7474  apreap  7578  apreim  7594  zltlen  8319  prime  8337  fzind  8353  qltlen  8575  xltnegi  8748  ixxval  8765  fzval  8876  fzdifsuc  8943  elfzm11  8953  elfzo  9006  qbtwnzlemshrink  9104  rebtwn2zlemshrink  9108  shftfvalg  9419  shftfibg  9421  shftfval  9422  shftfib  9424  shftfn  9425  2shfti  9432  cau3lem  9710  caubnd2  9713  clim  9802  clim2  9804  climi  9808  climcn2  9830  addcn2  9831  subcn2  9832  mulcn2  9833  algcvgblem  9888