Theorem anbi1d 465

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ 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:  anbi1  466  anbi12d  473  bi2anan9  608  pm5.71dc  967  dfifp4dc  989  dfifp5dc  990  xorbi1d  1423  drsb1  1845  ax11ev  1874  eleq1w  2290  eleq1  2292  rexeqf  2725  reueq1f  2726  rmoeq1f  2727  rabeqf  2789  vtocl2gaf  2868  alexeq  2929  ceqex  2930  elrabi  2956  sbc5  3052  rexss  3291  ineq1  3398  difin2  3466  r19.28m  3581  elif  3614  preq12bg  3851  opeq1  3857  eluni  3891  disjiun  4078  mpteq12f  4164  axsep2  4203  zfauscl  4204  opthg  4324  copsexg  4330  euotd  4341  elopab  4346  pocl  4394  uniuni  4542  rabxfrd  4560  ontr2exmid  4617  regexmidlemm  4624  regexmidlem1  4625  reg2exmidlema  4626  preleq  4647  xpeq1  4733  elxpi  4735  vtoclr  4767  opbrop  4798  opelresg  5012  resopab2  5052  elxp4  5216  elxp5  5217  cnvpom  5271  fun11  5388  feq2  5457  f1eq2  5529  f1eq3  5530  foeq2  5547  brprcneu  5622  ssimaexg  5698  dmfco  5704  fndmdif  5742  rexsupp  5761  respreima  5765  isoeq5  5935  isoini  5948  isopolem  5952  f1oiso  5956  f1oiso2  5957  riotaeqdv  5961  acexmidlemab  6001  acexmidlemcase  6002  oprabid  6039  mpoeq123  6069  mpoeq123dva  6071  eloprabga  6097  resoprab  6106  resoprab2  6107  ov  6130  ovi3  6148  ov6g  6149  ovg  6150  caoftrn  6257  opabex3d  6272  opabex3  6273  elxp7  6322  eloprabi  6348  cnvf1o  6377  xporderlem  6383  poxp  6384  smoel2  6455  frec0g  6549  freccllem  6554  frecfcllem  6556  frecsuclem  6558  frecsuc  6559  nnaordex  6682  qliftel  6770  brecop  6780  eroveu  6781  ecopovtrn  6787  ecopovtrng  6790  th3qlem2  6793  th3q  6795  ixpsnf1o  6891  dom2lem  6931  xpsnen  6988  xpassen  6997  pw2f1odclem  7003  xpf1o  7013  opabfi  7111  ctssdccl  7289  exmidapne  7457  dfplpq2  7552  dfmpq2  7553  ltsonq  7596  enq0sym  7630  enq0ref  7631  enq0tr  7632  enq0breq  7634  addnq0mo  7645  mulnq0mo  7646  addnnnq0  7647  mulnnnq0  7648  elinp  7672  prnmaxl  7686  prnminu  7687  prarloclemlo  7692  prarloc  7701  genpdflem  7705  genpassl  7722  genpassu  7723  ltexprlemm  7798  recexprlemell  7820  recexprlemelu  7821  cauappcvgprlemdisj  7849  caucvgprlemnkj  7864  caucvgprprlemnkltj  7887  caucvgprprlemnkeqj  7888  addsrmo  7941  mulsrmo  7942  addsrpr  7943  mulsrpr  7944  lttrsr  7960  mulgt0sr  7976  ltresr  8037  axpre-lttrn  8082  axpre-mulgt0  8085  recexgt0  8738  apreap  8745  apreim  8761  aprcl  8804  aptap  8808  prime  9557  rexuz  9787  ltxr  9983  ixxval  10104  fzval  10218  eqwrd  11125  pfxeq  11243  wrd2ind  11270  sqrtrval  11526  abslt  11614  absle  11615  lenegsq  11621  abs2difabs  11634  2clim  11827  climcn2  11835  addcn2  11836  mulcn2  11838  climrecvg1n  11874  sumeq1  11881  fsum2dlemstep  11960  modfsummod  11984  prodeq1f  12078  fprod2dlemstep  12148  nndivdvds  12322  divalg2  12452  gcdval  12495  bezoutlemstep  12533  bezoutlemmain  12534  bezoutlemex  12537  gcdass  12551  lcmval  12600  lcmass  12622  rpexp  12690  pythagtriplem2  12804  pythagtrip  12821  gsumfzval  13439  issgrpv  13452  issgrpn0  13453  ismhm  13509  mhmpropd  13514  issubm  13520  issubg  13725  issubg3  13744  ringpropd  14016  crngpropd  14017  opprunitd  14089  issubrg  14200  resrhm2b  14228  islmod  14270  lmodlema  14271  lmodprop2d  14327  islssm  14336  islssmg  14337  lsslss  14360  znleval  14632  psrbag  14648  istopg  14688  basis2  14737  tg2  14749  iscld  14792  neival  14832  isnei  14833  isneip  14835  iscn  14886  cnpval  14887  iscnp  14888  txbas  14947  txdis1cn  14967  ispsmet  15012  ismet  15033  isxmet  15034  ismet2  15043  blres  15123  elmopn  15135  mopni  15171  neibl  15180  metrest  15195  elcncf  15262  mulc1cncf  15278  mulcncf  15297  limccnp2lem  15365  sincosq2sgn  15516  sincosq4sgn  15518  2lgslem1a  15782  edgssv2en  16012  uhgr2edg  16019  vtxdfifiun  16056  trlsfvalg  16122  istrl  16124  bdsep2  16304  bdzfauscl  16308  bj-d0clsepcl  16343  sscoll2  16406