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  606  pm5.71dc  963  xorbi1d  1392  drsb1  1813  ax11ev  1842  eleq1w  2257  eleq1  2259  rexeqf  2690  reueq1f  2691  rmoeq1f  2692  rabeqf  2753  vtocl2gaf  2831  alexeq  2890  ceqex  2891  elrabi  2917  sbc5  3013  rexss  3251  ineq1  3358  difin2  3426  r19.28m  3541  preq12bg  3804  opeq1  3809  eluni  3843  disjiun  4029  mpteq12f  4114  axsep2  4153  zfauscl  4154  opthg  4272  copsexg  4278  euotd  4288  elopab  4293  pocl  4339  uniuni  4487  rabxfrd  4505  ontr2exmid  4562  regexmidlemm  4569  regexmidlem1  4570  reg2exmidlema  4571  preleq  4592  xpeq1  4678  elxpi  4680  vtoclr  4712  opbrop  4743  opelresg  4954  resopab2  4994  elxp4  5158  elxp5  5159  cnvpom  5213  fun11  5326  feq2  5394  f1eq2  5462  f1eq3  5463  foeq2  5480  brprcneu  5554  ssimaexg  5626  dmfco  5632  fndmdif  5670  rexsupp  5689  respreima  5693  isoeq5  5855  isoini  5868  isopolem  5872  f1oiso  5876  f1oiso2  5877  riotaeqdv  5881  acexmidlemab  5919  acexmidlemcase  5920  oprabid  5957  mpoeq123  5985  mpoeq123dva  5987  eloprabga  6013  resoprab  6022  resoprab2  6023  ov  6046  ovi3  6064  ov6g  6065  ovg  6066  caoftrn  6172  opabex3d  6187  opabex3  6188  elxp7  6237  eloprabi  6263  cnvf1o  6292  xporderlem  6298  poxp  6299  smoel2  6370  frec0g  6464  freccllem  6469  frecfcllem  6471  frecsuclem  6473  frecsuc  6474  nnaordex  6595  qliftel  6683  brecop  6693  eroveu  6694  ecopovtrn  6700  ecopovtrng  6703  th3qlem2  6706  th3q  6708  ixpsnf1o  6804  dom2lem  6840  xpsnen  6889  xpassen  6898  pw2f1odclem  6904  xpf1o  6914  opabfi  7008  ctssdccl  7186  exmidapne  7345  dfplpq2  7440  dfmpq2  7441  ltsonq  7484  enq0sym  7518  enq0ref  7519  enq0tr  7520  enq0breq  7522  addnq0mo  7533  mulnq0mo  7534  addnnnq0  7535  mulnnnq0  7536  elinp  7560  prnmaxl  7574  prnminu  7575  prarloclemlo  7580  prarloc  7589  genpdflem  7593  genpassl  7610  genpassu  7611  ltexprlemm  7686  recexprlemell  7708  recexprlemelu  7709  cauappcvgprlemdisj  7737  caucvgprlemnkj  7752  caucvgprprlemnkltj  7775  caucvgprprlemnkeqj  7776  addsrmo  7829  mulsrmo  7830  addsrpr  7831  mulsrpr  7832  lttrsr  7848  mulgt0sr  7864  ltresr  7925  axpre-lttrn  7970  axpre-mulgt0  7973  recexgt0  8626  apreap  8633  apreim  8649  aprcl  8692  aptap  8696  prime  9444  rexuz  9673  ltxr  9869  ixxval  9990  fzval  10104  eqwrd  10994  sqrtrval  11184  abslt  11272  absle  11273  lenegsq  11279  abs2difabs  11292  2clim  11485  climcn2  11493  addcn2  11494  mulcn2  11496  climrecvg1n  11532  sumeq1  11539  fsum2dlemstep  11618  modfsummod  11642  prodeq1f  11736  fprod2dlemstep  11806  nndivdvds  11980  divalg2  12110  gcdval  12153  bezoutlemstep  12191  bezoutlemmain  12192  bezoutlemex  12195  gcdass  12209  lcmval  12258  lcmass  12280  rpexp  12348  pythagtriplem2  12462  pythagtrip  12479  gsumfzval  13095  issgrpv  13108  issgrpn0  13109  ismhm  13165  mhmpropd  13170  issubm  13176  issubg  13381  issubg3  13400  ringpropd  13672  crngpropd  13673  opprunitd  13744  issubrg  13855  resrhm2b  13883  islmod  13925  lmodlema  13926  lmodprop2d  13982  islssm  13991  islssmg  13992  lsslss  14015  znleval  14287  psrbag  14303  istopg  14343  basis2  14392  tg2  14404  iscld  14447  neival  14487  isnei  14488  isneip  14490  iscn  14541  cnpval  14542  iscnp  14543  txbas  14602  txdis1cn  14622  ispsmet  14667  ismet  14688  isxmet  14689  ismet2  14698  blres  14778  elmopn  14790  mopni  14826  neibl  14835  metrest  14850  elcncf  14917  mulc1cncf  14933  mulcncf  14952  limccnp2lem  15020  sincosq2sgn  15171  sincosq4sgn  15173  2lgslem1a  15437  bdsep2  15640  bdzfauscl  15644  bj-d0clsepcl  15679  sscoll2  15742