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  610  pm5.71dc  970  dfifp4dc  992  dfifp5dc  993  xorbi1d  1426  drsb1  1848  ax11ev  1877  eleq1w  2295  eleq1  2297  rexeqf  2740  reueq1f  2741  rmoeq1f  2742  rabeqf  2805  vtocl2gaf  2884  alexeq  2946  ceqex  2947  elrabi  2973  sbc5  3069  rexss  3309  ineq1  3419  difin2  3487  r19.28m  3603  elif  3638  ifeqeqxdc  3673  rabsnifsb  3762  preq12bg  3882  opeq1  3888  eluni  3922  disjiun  4109  mpteq12f  4195  axsep2  4234  zfauscl  4235  opthg  4359  copsexg  4365  euotd  4376  elopab  4381  pocl  4429  uniuni  4577  rabxfrd  4595  ontr2exmid  4652  regexmidlemm  4659  regexmidlem1  4660  reg2exmidlema  4661  preleq  4682  xpeq1  4768  elxpi  4770  vtoclr  4803  opbrop  4834  opelresg  5050  resopab2  5090  elxp4  5255  elxp5  5256  cnvpom  5310  fun11  5428  feq2  5497  f1eq2  5574  f1eq3  5575  foeq2  5592  brprcneu  5668  ssimaexg  5744  dmfco  5750  fndmdif  5788  respreima  5810  isoeq5  5984  isoini  5997  isopolem  6001  f1oiso  6005  f1oiso2  6006  riotaeqdv  6012  acexmidlemab  6052  acexmidlemcase  6053  oprabid  6090  mpoeq123  6120  mpoeq123dva  6122  eloprabga  6148  resoprab  6157  resoprab2  6158  ov  6181  ovi3  6199  ov6g  6200  ovg  6201  caoftrn  6308  opabex3d  6323  opabex3  6324  elxp7  6377  eloprabi  6405  cnvf1o  6434  xporderlem  6440  poxp  6441  rexsupp  6466  smoel2  6547  frec0g  6641  freccllem  6646  frecfcllem  6648  frecsuclem  6650  frecsuc  6651  nnaordex  6774  qliftel  6862  brecop  6872  eroveu  6873  ecopovtrn  6879  ecopovtrng  6882  th3qlem2  6885  th3q  6887  ixpsnf1o  6984  dom2lem  7024  mapsnend  7065  modom  7074  xpsnen  7085  xpassen  7094  pw2f1odclem  7100  xpf1o  7110  opabfi  7213  ctssdccl  7415  exmidapne  7590  dfplpq2  7685  dfmpq2  7686  ltsonq  7729  enq0sym  7763  enq0ref  7764  enq0tr  7765  enq0breq  7767  addnq0mo  7778  mulnq0mo  7779  addnnnq0  7780  mulnnnq0  7781  elinp  7805  prnmaxl  7819  prnminu  7820  prarloclemlo  7825  prarloc  7834  genpdflem  7838  genpassl  7855  genpassu  7856  ltexprlemm  7931  recexprlemell  7953  recexprlemelu  7954  cauappcvgprlemdisj  7982  caucvgprlemnkj  7997  caucvgprprlemnkltj  8020  caucvgprprlemnkeqj  8021  addsrmo  8074  mulsrmo  8075  addsrpr  8076  mulsrpr  8077  lttrsr  8093  mulgt0sr  8109  ltresr  8170  axpre-lttrn  8215  axpre-mulgt0  8218  recexgt0  8871  apreap  8878  apreim  8894  aprcl  8937  aptap  8941  prime  9695  rexuz  9930  ltxr  10127  ixxval  10248  fzval  10363  hashfibclem  11231  eqwrd  11290  pfxeq  11413  wrd2ind  11440  sqrtrval  11710  abslt  11798  absle  11799  lenegsq  11805  abs2difabs  11818  2clim  12011  climcn2  12019  addcn2  12020  mulcn2  12022  climrecvg1n  12058  sumeq1  12065  fsum2dlemstep  12145  modfsummod  12169  prodeq1f  12263  fprod2dlemstep  12333  nndivdvds  12507  divalg2  12637  gcdval  12680  bezoutlemstep  12718  bezoutlemmain  12719  bezoutlemex  12722  gcdass  12736  lcmval  12785  lcmass  12807  rpexp  12875  pythagtriplem2  12989  pythagtrip  13006  gsumfzval  13654  issgrpv  13667  issgrpn0  13668  ismhm  13716  mhmpropd  13721  issubm  13727  issubg  13926  issubg3  13945  ringpropd  14281  crngpropd  14282  opprunitd  14355  issubrg  14467  resrhm2b  14495  islmod  14565  lmodlema  14566  lmodprop2d  14622  islssm  14631  islssmg  14632  lsslss  14655  znleval  14927  psrbag  14943  istopg  14990  basis2  15039  tg2  15051  iscld  15094  neival  15134  isnei  15135  isneip  15137  iscn  15188  cnpval  15189  iscnp  15190  txbas  15249  txdis1cn  15269  ispsmet  15314  ismet  15335  isxmet  15336  ismet2  15345  blres  15425  elmopn  15437  mopni  15473  neibl  15482  metrest  15497  elcncf  15564  mulc1cncf  15580  mulcncf  15599  limccnp2lem  15667  sincosq2sgn  15818  sincosq4sgn  15820  pellexlem3  15973  2lgslem1a  16087  edgssv2en  16320  uhgr2edg  16327  vtxdfifiun  16418  trlsfvalg  16504  istrl  16506  clwwlknp  16538  iseupth  16568  eupth2lem2dc  16580  bdsep2  16782  bdzfauscl  16786  bj-d0clsepcl  16821  sscoll2  16884