Theorem anbi1d 438

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 424	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:  anbi1  439  anbi12d  442  bi2anan9  538  pm5.71dc  868  xorbi1d  1272  drsb1  1680  ax11ev  1709  eleq1  2100  rexeqf  2502  reueq1f  2503  rmoeq1f  2504  rabeqf  2550  vtocl2gaf  2620  alexeq  2670  ceqex  2671  elrabi  2695  sbc5  2787  rexss  3007  psstr  3049  sspsstr  3050  ineq1  3131  difin2  3199  r19.28m  3311  preq12bg  3544  opeq1  3549  eluni  3583  mpteq12f  3837  axsep2  3876  zfauscl  3877  opthg  3975  copsexg  3981  euotd  3991  elopab  3995  pocl  4040  uniuni  4183  rabxfrd  4201  ontr2exmid  4250  regexmidlemm  4257  regexmidlem1  4258  reg2exmidlema  4259  preleq  4279  xpeq1  4359  elxpi  4361  vtoclr  4388  opbrop  4419  opelresg  4619  resopab2  4655  elxp4  4808  elxp5  4809  cnvpom  4860  fun11  4966  feq2  5031  f1eq2  5088  f1eq3  5089  foeq2  5103  brprcneu  5171  ssimaexg  5235  dmfco  5241  fndmdif  5272  rexsupp  5291  respreima  5295  isoeq5  5445  isoini  5457  isopolem  5461  f1oiso  5465  f1oiso2  5466  riotaeqdv  5469  acexmidlemab  5506  acexmidlemcase  5507  oprabid  5537  mpt2eq123  5564  mpt2eq123dva  5566  eloprabga  5591  resoprab  5597  resoprab2  5598  ov  5620  ovi3  5637  ov6g  5638  ovg  5639  caoftrn  5736  opabex3d  5748  opabex3  5749  elxp7  5797  eloprabi  5822  cnvf1o  5846  xporderlem  5852  poxp  5853  smoel2  5918  frec0g  5983  frecsuclem3  5990  frecsuc  5991  nnaordex  6100  qliftel  6186  brecop  6196  eroveu  6197  ecopovtrn  6203  ecopovtrng  6206  th3qlem2  6209  th3q  6211  dom2lem  6252  xpsnen  6295  xpassen  6304  dfplpq2  6452  dfmpq2  6453  ltsonq  6496  enq0sym  6530  enq0ref  6531  enq0tr  6532  enq0breq  6534  addnq0mo  6545  mulnq0mo  6546  addnnnq0  6547  mulnnnq0  6548  elinp  6572  prnmaxl  6586  prnminu  6587  prarloclemlo  6592  prarloc  6601  genpdflem  6605  genpassl  6622  genpassu  6623  ltexprlemm  6698  recexprlemell  6720  recexprlemelu  6721  cauappcvgprlemdisj  6749  caucvgprlemnkj  6764  caucvgprprlemnkltj  6787  caucvgprprlemnkeqj  6788  addsrmo  6828  mulsrmo  6829  addsrpr  6830  mulsrpr  6831  lttrsr  6847  mulgt0sr  6862  ltresr  6915  axpre-lttrn  6958  axpre-mulgt0  6961  recexgt0  7571  apreap  7578  apreim  7594  prime  8337  rexuz  8523  ltxr  8695  ixxval  8765  fzval  8876  sqrtrval  9598  abslt  9684  absle  9685  lenegsq  9691  abs2difabs  9704  2clim  9822  climcn2  9830  addcn2  9831  mulcn2  9833  climrecvg1n  9867  sumeq1  9874  bdsep2  10006  bdzfauscl  10010  bj-d0clsepcl  10049