Theorem anbi1d 461

Description: Deduction adding a right 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
anbi1d	⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜃)))

Proof of Theorem anbi1d

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

Syntax hints:   → wi 4   ∧ wa 103   ↔ 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:  anbi1  462  anbi12d  465  bi2anan9  596  pm5.71dc  951  xorbi1d  1371  drsb1  1787  ax11ev  1816  eleq1w  2227  eleq1  2229  rexeqf  2658  reueq1f  2659  rmoeq1f  2660  rabeqf  2716  vtocl2gaf  2793  alexeq  2852  ceqex  2853  elrabi  2879  sbc5  2974  rexss  3209  ineq1  3316  difin2  3384  r19.28m  3498  preq12bg  3753  opeq1  3758  eluni  3792  disjiun  3977  mpteq12f  4062  axsep2  4101  zfauscl  4102  opthg  4216  copsexg  4222  euotd  4232  elopab  4236  pocl  4281  uniuni  4429  rabxfrd  4447  ontr2exmid  4502  regexmidlemm  4509  regexmidlem1  4510  reg2exmidlema  4511  preleq  4532  xpeq1  4618  elxpi  4620  vtoclr  4652  opbrop  4683  opelresg  4891  resopab2  4931  elxp4  5091  elxp5  5092  cnvpom  5146  fun11  5255  feq2  5321  f1eq2  5389  f1eq3  5390  foeq2  5407  brprcneu  5479  ssimaexg  5548  dmfco  5554  fndmdif  5590  rexsupp  5609  respreima  5613  isoeq5  5773  isoini  5786  isopolem  5790  f1oiso  5794  f1oiso2  5795  riotaeqdv  5799  acexmidlemab  5836  acexmidlemcase  5837  oprabid  5874  mpoeq123  5901  mpoeq123dva  5903  eloprabga  5929  resoprab  5938  resoprab2  5939  ov  5961  ovi3  5978  ov6g  5979  ovg  5980  caoftrn  6075  opabex3d  6089  opabex3  6090  elxp7  6138  eloprabi  6164  cnvf1o  6193  xporderlem  6199  poxp  6200  smoel2  6271  frec0g  6365  freccllem  6370  frecfcllem  6372  frecsuclem  6374  frecsuc  6375  nnaordex  6495  qliftel  6581  brecop  6591  eroveu  6592  ecopovtrn  6598  ecopovtrng  6601  th3qlem2  6604  th3q  6606  ixpsnf1o  6702  dom2lem  6738  xpsnen  6787  xpassen  6796  xpf1o  6810  ctssdccl  7076  dfplpq2  7295  dfmpq2  7296  ltsonq  7339  enq0sym  7373  enq0ref  7374  enq0tr  7375  enq0breq  7377  addnq0mo  7388  mulnq0mo  7389  addnnnq0  7390  mulnnnq0  7391  elinp  7415  prnmaxl  7429  prnminu  7430  prarloclemlo  7435  prarloc  7444  genpdflem  7448  genpassl  7465  genpassu  7466  ltexprlemm  7541  recexprlemell  7563  recexprlemelu  7564  cauappcvgprlemdisj  7592  caucvgprlemnkj  7607  caucvgprprlemnkltj  7630  caucvgprprlemnkeqj  7631  addsrmo  7684  mulsrmo  7685  addsrpr  7686  mulsrpr  7687  lttrsr  7703  mulgt0sr  7719  ltresr  7780  axpre-lttrn  7825  axpre-mulgt0  7828  recexgt0  8478  apreap  8485  apreim  8501  aprcl  8544  prime  9290  rexuz  9518  ltxr  9711  ixxval  9832  fzval  9946  sqrtrval  10942  abslt  11030  absle  11031  lenegsq  11037  abs2difabs  11050  2clim  11242  climcn2  11250  addcn2  11251  mulcn2  11253  climrecvg1n  11289  sumeq1  11296  fsum2dlemstep  11375  modfsummod  11399  prodeq1f  11493  fprod2dlemstep  11563  nndivdvds  11736  divalg2  11863  gcdval  11892  bezoutlemstep  11930  bezoutlemmain  11931  bezoutlemex  11934  gcdass  11948  lcmval  11995  lcmass  12017  rpexp  12085  pythagtriplem2  12198  pythagtrip  12215  istopg  12637  basis2  12686  tg2  12700  iscld  12743  neival  12783  isnei  12784  isneip  12786  iscn  12837  cnpval  12838  iscnp  12839  txbas  12898  txdis1cn  12918  ispsmet  12963  ismet  12984  isxmet  12985  ismet2  12994  blres  13074  elmopn  13086  mopni  13122  neibl  13131  metrest  13146  elcncf  13200  mulc1cncf  13216  mulcncf  13231  limccnp2lem  13285  sincosq2sgn  13388  sincosq4sgn  13390  bdsep2  13768  bdzfauscl  13772  bj-d0clsepcl  13807  sscoll2  13870