Theorem anbi1d 456

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 442	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  anbi1  457  anbi12d  460  bi2anan9  576  pm5.71dc  913  xorbi1d  1327  drsb1  1738  ax11ev  1767  eleq1w  2160  eleq1  2162  rexeqf  2581  reueq1f  2582  rmoeq1f  2583  rabeqf  2631  vtocl2gaf  2708  alexeq  2765  ceqex  2766  elrabi  2790  sbc5  2885  rexss  3111  ineq1  3217  difin2  3285  r19.28m  3399  preq12bg  3647  opeq1  3652  eluni  3686  disjiun  3870  mpteq12f  3948  axsep2  3987  zfauscl  3988  opthg  4098  copsexg  4104  euotd  4114  elopab  4118  pocl  4163  uniuni  4310  rabxfrd  4328  ontr2exmid  4378  regexmidlemm  4385  regexmidlem1  4386  reg2exmidlema  4387  preleq  4408  xpeq1  4491  elxpi  4493  vtoclr  4525  opbrop  4556  opelresg  4762  resopab2  4802  elxp4  4962  elxp5  4963  cnvpom  5017  fun11  5126  feq2  5192  f1eq2  5260  f1eq3  5261  foeq2  5278  brprcneu  5346  ssimaexg  5415  dmfco  5421  fndmdif  5457  rexsupp  5476  respreima  5480  isoeq5  5638  isoini  5651  isopolem  5655  f1oiso  5659  f1oiso2  5660  riotaeqdv  5663  acexmidlemab  5700  acexmidlemcase  5701  oprabid  5735  mpoeq123  5762  mpoeq123dva  5764  eloprabga  5790  resoprab  5799  resoprab2  5800  ov  5822  ovi3  5839  ov6g  5840  ovg  5841  caoftrn  5938  opabex3d  5950  opabex3  5951  elxp7  5999  eloprabi  6024  cnvf1o  6052  xporderlem  6058  poxp  6059  smoel2  6130  frec0g  6224  freccllem  6229  frecfcllem  6231  frecsuclem  6233  frecsuc  6234  nnaordex  6353  qliftel  6439  brecop  6449  eroveu  6450  ecopovtrn  6456  ecopovtrng  6459  th3qlem2  6462  th3q  6464  ixpsnf1o  6560  dom2lem  6596  xpsnen  6644  xpassen  6653  xpf1o  6667  ctssdclemr  6911  dfplpq2  7063  dfmpq2  7064  ltsonq  7107  enq0sym  7141  enq0ref  7142  enq0tr  7143  enq0breq  7145  addnq0mo  7156  mulnq0mo  7157  addnnnq0  7158  mulnnnq0  7159  elinp  7183  prnmaxl  7197  prnminu  7198  prarloclemlo  7203  prarloc  7212  genpdflem  7216  genpassl  7233  genpassu  7234  ltexprlemm  7309  recexprlemell  7331  recexprlemelu  7332  cauappcvgprlemdisj  7360  caucvgprlemnkj  7375  caucvgprprlemnkltj  7398  caucvgprprlemnkeqj  7399  addsrmo  7439  mulsrmo  7440  addsrpr  7441  mulsrpr  7442  lttrsr  7458  mulgt0sr  7473  ltresr  7526  axpre-lttrn  7569  axpre-mulgt0  7572  recexgt0  8208  apreap  8215  apreim  8231  prime  9002  rexuz  9225  ltxr  9403  ixxval  9520  fzval  9633  sqrtrval  10612  abslt  10700  absle  10701  lenegsq  10707  abs2difabs  10720  2clim  10909  climcn2  10917  addcn2  10918  mulcn2  10920  climrecvg1n  10956  sumeq1  10963  fsum2dlemstep  11042  modfsummod  11066  nndivdvds  11294  divalg2  11418  gcdval  11443  bezoutlemstep  11478  bezoutlemmain  11479  bezoutlemex  11482  gcdass  11496  lcmval  11537  lcmass  11559  rpexp  11624  istopg  11948  basis2  11997  tg2  12011  iscld  12054  neival  12094  isnei  12095  isneip  12097  iscn  12147  cnpval  12148  iscnp  12149  txbas  12208  txdis1cn  12228  ispsmet  12251  ismet  12272  isxmet  12273  ismet2  12282  blres  12362  elmopn  12374  mopni  12410  neibl  12419  metrest  12434  elcncf  12473  mulc1cncf  12489  mulcncf  12503  bdsep2  12665  bdzfauscl  12669  bj-d0clsepcl  12708