Theorem anbi1d 462

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 448	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  anbi1  463  anbi12d  470  bi2anan9  601  pm5.71dc  956  xorbi1d  1376  drsb1  1792  ax11ev  1821  eleq1w  2231  eleq1  2233  rexeqf  2662  reueq1f  2663  rmoeq1f  2664  rabeqf  2720  vtocl2gaf  2797  alexeq  2856  ceqex  2857  elrabi  2883  sbc5  2978  rexss  3214  ineq1  3321  difin2  3389  r19.28m  3503  preq12bg  3758  opeq1  3763  eluni  3797  disjiun  3982  mpteq12f  4067  axsep2  4106  zfauscl  4107  opthg  4221  copsexg  4227  euotd  4237  elopab  4241  pocl  4286  uniuni  4434  rabxfrd  4452  ontr2exmid  4507  regexmidlemm  4514  regexmidlem1  4515  reg2exmidlema  4516  preleq  4537  xpeq1  4623  elxpi  4625  vtoclr  4657  opbrop  4688  opelresg  4896  resopab2  4936  elxp4  5096  elxp5  5097  cnvpom  5151  fun11  5263  feq2  5329  f1eq2  5397  f1eq3  5398  foeq2  5415  brprcneu  5487  ssimaexg  5556  dmfco  5562  fndmdif  5598  rexsupp  5617  respreima  5621  isoeq5  5781  isoini  5794  isopolem  5798  f1oiso  5802  f1oiso2  5803  riotaeqdv  5807  acexmidlemab  5844  acexmidlemcase  5845  oprabid  5882  mpoeq123  5909  mpoeq123dva  5911  eloprabga  5937  resoprab  5946  resoprab2  5947  ov  5969  ovi3  5986  ov6g  5987  ovg  5988  caoftrn  6083  opabex3d  6097  opabex3  6098  elxp7  6146  eloprabi  6172  cnvf1o  6201  xporderlem  6207  poxp  6208  smoel2  6279  frec0g  6373  freccllem  6378  frecfcllem  6380  frecsuclem  6382  frecsuc  6383  nnaordex  6503  qliftel  6589  brecop  6599  eroveu  6600  ecopovtrn  6606  ecopovtrng  6609  th3qlem2  6612  th3q  6614  ixpsnf1o  6710  dom2lem  6746  xpsnen  6795  xpassen  6804  xpf1o  6818  ctssdccl  7084  dfplpq2  7303  dfmpq2  7304  ltsonq  7347  enq0sym  7381  enq0ref  7382  enq0tr  7383  enq0breq  7385  addnq0mo  7396  mulnq0mo  7397  addnnnq0  7398  mulnnnq0  7399  elinp  7423  prnmaxl  7437  prnminu  7438  prarloclemlo  7443  prarloc  7452  genpdflem  7456  genpassl  7473  genpassu  7474  ltexprlemm  7549  recexprlemell  7571  recexprlemelu  7572  cauappcvgprlemdisj  7600  caucvgprlemnkj  7615  caucvgprprlemnkltj  7638  caucvgprprlemnkeqj  7639  addsrmo  7692  mulsrmo  7693  addsrpr  7694  mulsrpr  7695  lttrsr  7711  mulgt0sr  7727  ltresr  7788  axpre-lttrn  7833  axpre-mulgt0  7836  recexgt0  8486  apreap  8493  apreim  8509  aprcl  8552  prime  9298  rexuz  9526  ltxr  9719  ixxval  9840  fzval  9954  sqrtrval  10951  abslt  11039  absle  11040  lenegsq  11046  abs2difabs  11059  2clim  11251  climcn2  11259  addcn2  11260  mulcn2  11262  climrecvg1n  11298  sumeq1  11305  fsum2dlemstep  11384  modfsummod  11408  prodeq1f  11502  fprod2dlemstep  11572  nndivdvds  11745  divalg2  11872  gcdval  11901  bezoutlemstep  11939  bezoutlemmain  11940  bezoutlemex  11943  gcdass  11957  lcmval  12004  lcmass  12026  rpexp  12094  pythagtriplem2  12207  pythagtrip  12224  issgrpv  12632  issgrpn0  12633  ismhm  12672  mhmpropd  12676  issubm  12682  istopg  12750  basis2  12799  tg2  12813  iscld  12856  neival  12896  isnei  12897  isneip  12899  iscn  12950  cnpval  12951  iscnp  12952  txbas  13011  txdis1cn  13031  ispsmet  13076  ismet  13097  isxmet  13098  ismet2  13107  blres  13187  elmopn  13199  mopni  13235  neibl  13244  metrest  13259  elcncf  13313  mulc1cncf  13329  mulcncf  13344  limccnp2lem  13398  sincosq2sgn  13501  sincosq4sgn  13503  bdsep2  13881  bdzfauscl  13885  bj-d0clsepcl  13920  sscoll2  13983