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  963  xorbi1d  1400  drsb1  1821  ax11ev  1850  eleq1w  2265  eleq1  2267  rexeqf  2698  reueq1f  2699  rmoeq1f  2700  rabeqf  2761  vtocl2gaf  2839  alexeq  2898  ceqex  2899  elrabi  2925  sbc5  3021  rexss  3259  ineq1  3366  difin2  3434  r19.28m  3549  preq12bg  3813  opeq1  3818  eluni  3852  disjiun  4038  mpteq12f  4123  axsep2  4162  zfauscl  4163  opthg  4281  copsexg  4287  euotd  4297  elopab  4302  pocl  4348  uniuni  4496  rabxfrd  4514  ontr2exmid  4571  regexmidlemm  4578  regexmidlem1  4579  reg2exmidlema  4580  preleq  4601  xpeq1  4687  elxpi  4689  vtoclr  4721  opbrop  4752  opelresg  4963  resopab2  5003  elxp4  5167  elxp5  5168  cnvpom  5222  fun11  5335  feq2  5403  f1eq2  5471  f1eq3  5472  foeq2  5489  brprcneu  5563  ssimaexg  5635  dmfco  5641  fndmdif  5679  rexsupp  5698  respreima  5702  isoeq5  5864  isoini  5877  isopolem  5881  f1oiso  5885  f1oiso2  5886  riotaeqdv  5890  acexmidlemab  5928  acexmidlemcase  5929  oprabid  5966  mpoeq123  5994  mpoeq123dva  5996  eloprabga  6022  resoprab  6031  resoprab2  6032  ov  6055  ovi3  6073  ov6g  6074  ovg  6075  caoftrn  6181  opabex3d  6196  opabex3  6197  elxp7  6246  eloprabi  6272  cnvf1o  6301  xporderlem  6307  poxp  6308  smoel2  6379  frec0g  6473  freccllem  6478  frecfcllem  6480  frecsuclem  6482  frecsuc  6483  nnaordex  6604  qliftel  6692  brecop  6702  eroveu  6703  ecopovtrn  6709  ecopovtrng  6712  th3qlem2  6715  th3q  6717  ixpsnf1o  6813  dom2lem  6849  xpsnen  6898  xpassen  6907  pw2f1odclem  6913  xpf1o  6923  opabfi  7017  ctssdccl  7195  exmidapne  7354  dfplpq2  7449  dfmpq2  7450  ltsonq  7493  enq0sym  7527  enq0ref  7528  enq0tr  7529  enq0breq  7531  addnq0mo  7542  mulnq0mo  7543  addnnnq0  7544  mulnnnq0  7545  elinp  7569  prnmaxl  7583  prnminu  7584  prarloclemlo  7589  prarloc  7598  genpdflem  7602  genpassl  7619  genpassu  7620  ltexprlemm  7695  recexprlemell  7717  recexprlemelu  7718  cauappcvgprlemdisj  7746  caucvgprlemnkj  7761  caucvgprprlemnkltj  7784  caucvgprprlemnkeqj  7785  addsrmo  7838  mulsrmo  7839  addsrpr  7840  mulsrpr  7841  lttrsr  7857  mulgt0sr  7873  ltresr  7934  axpre-lttrn  7979  axpre-mulgt0  7982  recexgt0  8635  apreap  8642  apreim  8658  aprcl  8701  aptap  8705  prime  9454  rexuz  9683  ltxr  9879  ixxval  10000  fzval  10114  eqwrd  11009  sqrtrval  11230  abslt  11318  absle  11319  lenegsq  11325  abs2difabs  11338  2clim  11531  climcn2  11539  addcn2  11540  mulcn2  11542  climrecvg1n  11578  sumeq1  11585  fsum2dlemstep  11664  modfsummod  11688  prodeq1f  11782  fprod2dlemstep  11852  nndivdvds  12026  divalg2  12156  gcdval  12199  bezoutlemstep  12237  bezoutlemmain  12238  bezoutlemex  12241  gcdass  12255  lcmval  12304  lcmass  12326  rpexp  12394  pythagtriplem2  12508  pythagtrip  12525  gsumfzval  13141  issgrpv  13154  issgrpn0  13155  ismhm  13211  mhmpropd  13216  issubm  13222  issubg  13427  issubg3  13446  ringpropd  13718  crngpropd  13719  opprunitd  13790  issubrg  13901  resrhm2b  13929  islmod  13971  lmodlema  13972  lmodprop2d  14028  islssm  14037  islssmg  14038  lsslss  14061  znleval  14333  psrbag  14349  istopg  14389  basis2  14438  tg2  14450  iscld  14493  neival  14533  isnei  14534  isneip  14536  iscn  14587  cnpval  14588  iscnp  14589  txbas  14648  txdis1cn  14668  ispsmet  14713  ismet  14734  isxmet  14735  ismet2  14744  blres  14824  elmopn  14836  mopni  14872  neibl  14881  metrest  14896  elcncf  14963  mulc1cncf  14979  mulcncf  14998  limccnp2lem  15066  sincosq2sgn  15217  sincosq4sgn  15219  2lgslem1a  15483  bdsep2  15686  bdzfauscl  15690  bj-d0clsepcl  15725  sscoll2  15788