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  3850  opeq1  3856  eluni  3890  disjiun  4077  mpteq12f  4163  axsep2  4202  zfauscl  4203  opthg  4323  copsexg  4329  euotd  4340  elopab  4345  pocl  4393  uniuni  4541  rabxfrd  4559  ontr2exmid  4616  regexmidlemm  4623  regexmidlem1  4624  reg2exmidlema  4625  preleq  4646  xpeq1  4732  elxpi  4734  vtoclr  4766  opbrop  4797  opelresg  5011  resopab2  5051  elxp4  5215  elxp5  5216  cnvpom  5270  fun11  5387  feq2  5456  f1eq2  5526  f1eq3  5527  foeq2  5544  brprcneu  5619  ssimaexg  5695  dmfco  5701  fndmdif  5739  rexsupp  5758  respreima  5762  isoeq5  5928  isoini  5941  isopolem  5945  f1oiso  5949  f1oiso2  5950  riotaeqdv  5954  acexmidlemab  5994  acexmidlemcase  5995  oprabid  6032  mpoeq123  6062  mpoeq123dva  6064  eloprabga  6090  resoprab  6099  resoprab2  6100  ov  6123  ovi3  6141  ov6g  6142  ovg  6143  caoftrn  6249  opabex3d  6264  opabex3  6265  elxp7  6314  eloprabi  6340  cnvf1o  6369  xporderlem  6375  poxp  6376  smoel2  6447  frec0g  6541  freccllem  6546  frecfcllem  6548  frecsuclem  6550  frecsuc  6551  nnaordex  6672  qliftel  6760  brecop  6770  eroveu  6771  ecopovtrn  6777  ecopovtrng  6780  th3qlem2  6783  th3q  6785  ixpsnf1o  6881  dom2lem  6921  xpsnen  6976  xpassen  6985  pw2f1odclem  6991  xpf1o  7001  opabfi  7096  ctssdccl  7274  exmidapne  7442  dfplpq2  7537  dfmpq2  7538  ltsonq  7581  enq0sym  7615  enq0ref  7616  enq0tr  7617  enq0breq  7619  addnq0mo  7630  mulnq0mo  7631  addnnnq0  7632  mulnnnq0  7633  elinp  7657  prnmaxl  7671  prnminu  7672  prarloclemlo  7677  prarloc  7686  genpdflem  7690  genpassl  7707  genpassu  7708  ltexprlemm  7783  recexprlemell  7805  recexprlemelu  7806  cauappcvgprlemdisj  7834  caucvgprlemnkj  7849  caucvgprprlemnkltj  7872  caucvgprprlemnkeqj  7873  addsrmo  7926  mulsrmo  7927  addsrpr  7928  mulsrpr  7929  lttrsr  7945  mulgt0sr  7961  ltresr  8022  axpre-lttrn  8067  axpre-mulgt0  8070  recexgt0  8723  apreap  8730  apreim  8746  aprcl  8789  aptap  8793  prime  9542  rexuz  9771  ltxr  9967  ixxval  10088  fzval  10202  eqwrd  11107  pfxeq  11223  wrd2ind  11250  sqrtrval  11506  abslt  11594  absle  11595  lenegsq  11601  abs2difabs  11614  2clim  11807  climcn2  11815  addcn2  11816  mulcn2  11818  climrecvg1n  11854  sumeq1  11861  fsum2dlemstep  11940  modfsummod  11964  prodeq1f  12058  fprod2dlemstep  12128  nndivdvds  12302  divalg2  12432  gcdval  12475  bezoutlemstep  12513  bezoutlemmain  12514  bezoutlemex  12517  gcdass  12531  lcmval  12580  lcmass  12602  rpexp  12670  pythagtriplem2  12784  pythagtrip  12801  gsumfzval  13419  issgrpv  13432  issgrpn0  13433  ismhm  13489  mhmpropd  13494  issubm  13500  issubg  13705  issubg3  13724  ringpropd  13996  crngpropd  13997  opprunitd  14068  issubrg  14179  resrhm2b  14207  islmod  14249  lmodlema  14250  lmodprop2d  14306  islssm  14315  islssmg  14316  lsslss  14339  znleval  14611  psrbag  14627  istopg  14667  basis2  14716  tg2  14728  iscld  14771  neival  14811  isnei  14812  isneip  14814  iscn  14865  cnpval  14866  iscnp  14867  txbas  14926  txdis1cn  14946  ispsmet  14991  ismet  15012  isxmet  15013  ismet2  15022  blres  15102  elmopn  15114  mopni  15150  neibl  15159  metrest  15174  elcncf  15241  mulc1cncf  15257  mulcncf  15276  limccnp2lem  15344  sincosq2sgn  15495  sincosq4sgn  15497  2lgslem1a  15761  edgssv2en  15991  uhgr2edg  15998  bdsep2  16207  bdzfauscl  16211  bj-d0clsepcl  16246  sscoll2  16309