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  961  xorbi1d  1381  drsb1  1799  ax11ev  1828  eleq1w  2238  eleq1  2240  rexeqf  2670  reueq1f  2671  rmoeq1f  2672  rabeqf  2729  vtocl2gaf  2806  alexeq  2865  ceqex  2866  elrabi  2892  sbc5  2988  rexss  3224  ineq1  3331  difin2  3399  r19.28m  3514  preq12bg  3775  opeq1  3780  eluni  3814  disjiun  4000  mpteq12f  4085  axsep2  4124  zfauscl  4125  opthg  4240  copsexg  4246  euotd  4256  elopab  4260  pocl  4305  uniuni  4453  rabxfrd  4471  ontr2exmid  4526  regexmidlemm  4533  regexmidlem1  4534  reg2exmidlema  4535  preleq  4556  xpeq1  4642  elxpi  4644  vtoclr  4676  opbrop  4707  opelresg  4916  resopab2  4956  elxp4  5118  elxp5  5119  cnvpom  5173  fun11  5285  feq2  5351  f1eq2  5419  f1eq3  5420  foeq2  5437  brprcneu  5510  ssimaexg  5580  dmfco  5586  fndmdif  5623  rexsupp  5642  respreima  5646  isoeq5  5808  isoini  5821  isopolem  5825  f1oiso  5829  f1oiso2  5830  riotaeqdv  5834  acexmidlemab  5871  acexmidlemcase  5872  oprabid  5909  mpoeq123  5936  mpoeq123dva  5938  eloprabga  5964  resoprab  5973  resoprab2  5974  ov  5996  ovi3  6013  ov6g  6014  ovg  6015  caoftrn  6110  opabex3d  6124  opabex3  6125  elxp7  6173  eloprabi  6199  cnvf1o  6228  xporderlem  6234  poxp  6235  smoel2  6306  frec0g  6400  freccllem  6405  frecfcllem  6407  frecsuclem  6409  frecsuc  6410  nnaordex  6531  qliftel  6617  brecop  6627  eroveu  6628  ecopovtrn  6634  ecopovtrng  6637  th3qlem2  6640  th3q  6642  ixpsnf1o  6738  dom2lem  6774  xpsnen  6823  xpassen  6832  xpf1o  6846  ctssdccl  7112  exmidapne  7261  dfplpq2  7355  dfmpq2  7356  ltsonq  7399  enq0sym  7433  enq0ref  7434  enq0tr  7435  enq0breq  7437  addnq0mo  7448  mulnq0mo  7449  addnnnq0  7450  mulnnnq0  7451  elinp  7475  prnmaxl  7489  prnminu  7490  prarloclemlo  7495  prarloc  7504  genpdflem  7508  genpassl  7525  genpassu  7526  ltexprlemm  7601  recexprlemell  7623  recexprlemelu  7624  cauappcvgprlemdisj  7652  caucvgprlemnkj  7667  caucvgprprlemnkltj  7690  caucvgprprlemnkeqj  7691  addsrmo  7744  mulsrmo  7745  addsrpr  7746  mulsrpr  7747  lttrsr  7763  mulgt0sr  7779  ltresr  7840  axpre-lttrn  7885  axpre-mulgt0  7888  recexgt0  8539  apreap  8546  apreim  8562  aprcl  8605  aptap  8609  prime  9354  rexuz  9582  ltxr  9777  ixxval  9898  fzval  10012  sqrtrval  11011  abslt  11099  absle  11100  lenegsq  11106  abs2difabs  11119  2clim  11311  climcn2  11319  addcn2  11320  mulcn2  11322  climrecvg1n  11358  sumeq1  11365  fsum2dlemstep  11444  modfsummod  11468  prodeq1f  11562  fprod2dlemstep  11632  nndivdvds  11805  divalg2  11933  gcdval  11962  bezoutlemstep  12000  bezoutlemmain  12001  bezoutlemex  12004  gcdass  12018  lcmval  12065  lcmass  12087  rpexp  12155  pythagtriplem2  12268  pythagtrip  12285  issgrpv  12815  issgrpn0  12816  ismhm  12858  mhmpropd  12862  issubm  12868  issubg  13038  issubg3  13057  ringpropd  13222  crngpropd  13223  opprunitd  13284  issubrg  13347  islmod  13386  lmodlema  13387  lmodprop2d  13443  islssm  13450  lsslss  13473  istopg  13584  basis2  13633  tg2  13645  iscld  13688  neival  13728  isnei  13729  isneip  13731  iscn  13782  cnpval  13783  iscnp  13784  txbas  13843  txdis1cn  13863  ispsmet  13908  ismet  13929  isxmet  13930  ismet2  13939  blres  14019  elmopn  14031  mopni  14067  neibl  14076  metrest  14091  elcncf  14145  mulc1cncf  14161  mulcncf  14176  limccnp2lem  14230  sincosq2sgn  14333  sincosq4sgn  14335  bdsep2  14723  bdzfauscl  14727  bj-d0clsepcl  14762  sscoll2  14825