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  2790  vtocl2gaf  2869  alexeq  2930  ceqex  2931  elrabi  2957  sbc5  3053  rexss  3292  ineq1  3399  difin2  3467  r19.28m  3582  elif  3615  rabsnifsb  3735  preq12bg  3854  opeq1  3860  eluni  3894  disjiun  4081  mpteq12f  4167  axsep2  4206  zfauscl  4207  opthg  4328  copsexg  4334  euotd  4345  elopab  4350  pocl  4398  uniuni  4546  rabxfrd  4564  ontr2exmid  4621  regexmidlemm  4628  regexmidlem1  4629  reg2exmidlema  4630  preleq  4651  xpeq1  4737  elxpi  4739  vtoclr  4772  opbrop  4803  opelresg  5018  resopab2  5058  elxp4  5222  elxp5  5223  cnvpom  5277  fun11  5394  feq2  5463  f1eq2  5535  f1eq3  5536  foeq2  5553  brprcneu  5628  ssimaexg  5704  dmfco  5710  fndmdif  5748  rexsupp  5767  respreima  5771  isoeq5  5941  isoini  5954  isopolem  5958  f1oiso  5962  f1oiso2  5963  riotaeqdv  5967  acexmidlemab  6007  acexmidlemcase  6008  oprabid  6045  mpoeq123  6075  mpoeq123dva  6077  eloprabga  6103  resoprab  6112  resoprab2  6113  ov  6136  ovi3  6154  ov6g  6155  ovg  6156  caoftrn  6263  opabex3d  6278  opabex3  6279  elxp7  6328  eloprabi  6356  cnvf1o  6385  xporderlem  6391  poxp  6392  smoel2  6464  frec0g  6558  freccllem  6563  frecfcllem  6565  frecsuclem  6567  frecsuc  6568  nnaordex  6691  qliftel  6779  brecop  6789  eroveu  6790  ecopovtrn  6796  ecopovtrng  6799  th3qlem2  6802  th3q  6804  ixpsnf1o  6900  dom2lem  6940  modom  6989  xpsnen  7000  xpassen  7009  pw2f1odclem  7015  xpf1o  7025  opabfi  7123  ctssdccl  7301  exmidapne  7469  dfplpq2  7564  dfmpq2  7565  ltsonq  7608  enq0sym  7642  enq0ref  7643  enq0tr  7644  enq0breq  7646  addnq0mo  7657  mulnq0mo  7658  addnnnq0  7659  mulnnnq0  7660  elinp  7684  prnmaxl  7698  prnminu  7699  prarloclemlo  7704  prarloc  7713  genpdflem  7717  genpassl  7734  genpassu  7735  ltexprlemm  7810  recexprlemell  7832  recexprlemelu  7833  cauappcvgprlemdisj  7861  caucvgprlemnkj  7876  caucvgprprlemnkltj  7899  caucvgprprlemnkeqj  7900  addsrmo  7953  mulsrmo  7954  addsrpr  7955  mulsrpr  7956  lttrsr  7972  mulgt0sr  7988  ltresr  8049  axpre-lttrn  8094  axpre-mulgt0  8097  recexgt0  8750  apreap  8757  apreim  8773  aprcl  8816  aptap  8820  prime  9569  rexuz  9804  ltxr  10000  ixxval  10121  fzval  10235  eqwrd  11144  pfxeq  11267  wrd2ind  11294  sqrtrval  11551  abslt  11639  absle  11640  lenegsq  11646  abs2difabs  11659  2clim  11852  climcn2  11860  addcn2  11861  mulcn2  11863  climrecvg1n  11899  sumeq1  11906  fsum2dlemstep  11985  modfsummod  12009  prodeq1f  12103  fprod2dlemstep  12173  nndivdvds  12347  divalg2  12477  gcdval  12520  bezoutlemstep  12558  bezoutlemmain  12559  bezoutlemex  12562  gcdass  12576  lcmval  12625  lcmass  12647  rpexp  12715  pythagtriplem2  12829  pythagtrip  12846  gsumfzval  13464  issgrpv  13477  issgrpn0  13478  ismhm  13534  mhmpropd  13539  issubm  13545  issubg  13750  issubg3  13769  ringpropd  14041  crngpropd  14042  opprunitd  14114  issubrg  14225  resrhm2b  14253  islmod  14295  lmodlema  14296  lmodprop2d  14352  islssm  14361  islssmg  14362  lsslss  14385  znleval  14657  psrbag  14673  istopg  14713  basis2  14762  tg2  14774  iscld  14817  neival  14857  isnei  14858  isneip  14860  iscn  14911  cnpval  14912  iscnp  14913  txbas  14972  txdis1cn  14992  ispsmet  15037  ismet  15058  isxmet  15059  ismet2  15068  blres  15148  elmopn  15160  mopni  15196  neibl  15205  metrest  15220  elcncf  15287  mulc1cncf  15303  mulcncf  15322  limccnp2lem  15390  sincosq2sgn  15541  sincosq4sgn  15543  2lgslem1a  15807  edgssv2en  16038  uhgr2edg  16045  vtxdfifiun  16103  trlsfvalg  16178  istrl  16180  clwwlknp  16212  iseupth  16242  bdsep2  16417  bdzfauscl  16421  bj-d0clsepcl  16456  sscoll2  16519