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  950  xorbi1d  1370  drsb1  1786  ax11ev  1815  eleq1w  2225  eleq1  2227  rexeqf  2656  reueq1f  2657  rmoeq1f  2658  rabeqf  2711  vtocl2gaf  2788  alexeq  2847  ceqex  2848  elrabi  2874  sbc5  2969  rexss  3204  ineq1  3311  difin2  3379  r19.28m  3493  preq12bg  3747  opeq1  3752  eluni  3786  disjiun  3971  mpteq12f  4056  axsep2  4095  zfauscl  4096  opthg  4210  copsexg  4216  euotd  4226  elopab  4230  pocl  4275  uniuni  4423  rabxfrd  4441  ontr2exmid  4496  regexmidlemm  4503  regexmidlem1  4504  reg2exmidlema  4505  preleq  4526  xpeq1  4612  elxpi  4614  vtoclr  4646  opbrop  4677  opelresg  4885  resopab2  4925  elxp4  5085  elxp5  5086  cnvpom  5140  fun11  5249  feq2  5315  f1eq2  5383  f1eq3  5384  foeq2  5401  brprcneu  5473  ssimaexg  5542  dmfco  5548  fndmdif  5584  rexsupp  5603  respreima  5607  isoeq5  5767  isoini  5780  isopolem  5784  f1oiso  5788  f1oiso2  5789  riotaeqdv  5793  acexmidlemab  5830  acexmidlemcase  5831  oprabid  5865  mpoeq123  5892  mpoeq123dva  5894  eloprabga  5920  resoprab  5929  resoprab2  5930  ov  5952  ovi3  5969  ov6g  5970  ovg  5971  caoftrn  6069  opabex3d  6081  opabex3  6082  elxp7  6130  eloprabi  6156  cnvf1o  6184  xporderlem  6190  poxp  6191  smoel2  6262  frec0g  6356  freccllem  6361  frecfcllem  6363  frecsuclem  6365  frecsuc  6366  nnaordex  6486  qliftel  6572  brecop  6582  eroveu  6583  ecopovtrn  6589  ecopovtrng  6592  th3qlem2  6595  th3q  6597  ixpsnf1o  6693  dom2lem  6729  xpsnen  6778  xpassen  6787  xpf1o  6801  ctssdccl  7067  dfplpq2  7286  dfmpq2  7287  ltsonq  7330  enq0sym  7364  enq0ref  7365  enq0tr  7366  enq0breq  7368  addnq0mo  7379  mulnq0mo  7380  addnnnq0  7381  mulnnnq0  7382  elinp  7406  prnmaxl  7420  prnminu  7421  prarloclemlo  7426  prarloc  7435  genpdflem  7439  genpassl  7456  genpassu  7457  ltexprlemm  7532  recexprlemell  7554  recexprlemelu  7555  cauappcvgprlemdisj  7583  caucvgprlemnkj  7598  caucvgprprlemnkltj  7621  caucvgprprlemnkeqj  7622  addsrmo  7675  mulsrmo  7676  addsrpr  7677  mulsrpr  7678  lttrsr  7694  mulgt0sr  7710  ltresr  7771  axpre-lttrn  7816  axpre-mulgt0  7819  recexgt0  8469  apreap  8476  apreim  8492  aprcl  8535  prime  9281  rexuz  9509  ltxr  9702  ixxval  9823  fzval  9937  sqrtrval  10928  abslt  11016  absle  11017  lenegsq  11023  abs2difabs  11036  2clim  11228  climcn2  11236  addcn2  11237  mulcn2  11239  climrecvg1n  11275  sumeq1  11282  fsum2dlemstep  11361  modfsummod  11385  prodeq1f  11479  fprod2dlemstep  11549  nndivdvds  11722  divalg2  11848  gcdval  11877  bezoutlemstep  11915  bezoutlemmain  11916  bezoutlemex  11919  gcdass  11933  lcmval  11974  lcmass  11996  rpexp  12062  pythagtriplem2  12175  pythagtrip  12192  istopg  12538  basis2  12587  tg2  12601  iscld  12644  neival  12684  isnei  12685  isneip  12687  iscn  12738  cnpval  12739  iscnp  12740  txbas  12799  txdis1cn  12819  ispsmet  12864  ismet  12885  isxmet  12886  ismet2  12895  blres  12975  elmopn  12987  mopni  13023  neibl  13032  metrest  13047  elcncf  13101  mulc1cncf  13117  mulcncf  13132  limccnp2lem  13186  sincosq2sgn  13289  sincosq4sgn  13291  bdsep2  13603  bdzfauscl  13607  bj-d0clsepcl  13642  sscoll2  13705