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  4298  elopab  4303  pocl  4349  uniuni  4497  rabxfrd  4515  ontr2exmid  4572  regexmidlemm  4579  regexmidlem1  4580  reg2exmidlema  4581  preleq  4602  xpeq1  4688  elxpi  4690  vtoclr  4722  opbrop  4753  opelresg  4965  resopab2  5005  elxp4  5169  elxp5  5170  cnvpom  5224  fun11  5340  feq2  5408  f1eq2  5476  f1eq3  5477  foeq2  5494  brprcneu  5568  ssimaexg  5640  dmfco  5646  fndmdif  5684  rexsupp  5703  respreima  5707  isoeq5  5873  isoini  5886  isopolem  5890  f1oiso  5894  f1oiso2  5895  riotaeqdv  5899  acexmidlemab  5937  acexmidlemcase  5938  oprabid  5975  mpoeq123  6003  mpoeq123dva  6005  eloprabga  6031  resoprab  6040  resoprab2  6041  ov  6064  ovi3  6082  ov6g  6083  ovg  6084  caoftrn  6190  opabex3d  6205  opabex3  6206  elxp7  6255  eloprabi  6281  cnvf1o  6310  xporderlem  6316  poxp  6317  smoel2  6388  frec0g  6482  freccllem  6487  frecfcllem  6489  frecsuclem  6491  frecsuc  6492  nnaordex  6613  qliftel  6701  brecop  6711  eroveu  6712  ecopovtrn  6718  ecopovtrng  6721  th3qlem2  6724  th3q  6726  ixpsnf1o  6822  dom2lem  6862  xpsnen  6915  xpassen  6924  pw2f1odclem  6930  xpf1o  6940  opabfi  7034  ctssdccl  7212  exmidapne  7371  dfplpq2  7466  dfmpq2  7467  ltsonq  7510  enq0sym  7544  enq0ref  7545  enq0tr  7546  enq0breq  7548  addnq0mo  7559  mulnq0mo  7560  addnnnq0  7561  mulnnnq0  7562  elinp  7586  prnmaxl  7600  prnminu  7601  prarloclemlo  7606  prarloc  7615  genpdflem  7619  genpassl  7636  genpassu  7637  ltexprlemm  7712  recexprlemell  7734  recexprlemelu  7735  cauappcvgprlemdisj  7763  caucvgprlemnkj  7778  caucvgprprlemnkltj  7801  caucvgprprlemnkeqj  7802  addsrmo  7855  mulsrmo  7856  addsrpr  7857  mulsrpr  7858  lttrsr  7874  mulgt0sr  7890  ltresr  7951  axpre-lttrn  7996  axpre-mulgt0  7999  recexgt0  8652  apreap  8659  apreim  8675  aprcl  8718  aptap  8722  prime  9471  rexuz  9700  ltxr  9896  ixxval  10017  fzval  10131  eqwrd  11032  sqrtrval  11253  abslt  11341  absle  11342  lenegsq  11348  abs2difabs  11361  2clim  11554  climcn2  11562  addcn2  11563  mulcn2  11565  climrecvg1n  11601  sumeq1  11608  fsum2dlemstep  11687  modfsummod  11711  prodeq1f  11805  fprod2dlemstep  11875  nndivdvds  12049  divalg2  12179  gcdval  12222  bezoutlemstep  12260  bezoutlemmain  12261  bezoutlemex  12264  gcdass  12278  lcmval  12327  lcmass  12349  rpexp  12417  pythagtriplem2  12531  pythagtrip  12548  gsumfzval  13165  issgrpv  13178  issgrpn0  13179  ismhm  13235  mhmpropd  13240  issubm  13246  issubg  13451  issubg3  13470  ringpropd  13742  crngpropd  13743  opprunitd  13814  issubrg  13925  resrhm2b  13953  islmod  13995  lmodlema  13996  lmodprop2d  14052  islssm  14061  islssmg  14062  lsslss  14085  znleval  14357  psrbag  14373  istopg  14413  basis2  14462  tg2  14474  iscld  14517  neival  14557  isnei  14558  isneip  14560  iscn  14611  cnpval  14612  iscnp  14613  txbas  14672  txdis1cn  14692  ispsmet  14737  ismet  14758  isxmet  14759  ismet2  14768  blres  14848  elmopn  14860  mopni  14896  neibl  14905  metrest  14920  elcncf  14987  mulc1cncf  15003  mulcncf  15022  limccnp2lem  15090  sincosq2sgn  15241  sincosq4sgn  15243  2lgslem1a  15507  bdsep2  15755  bdzfauscl  15759  bj-d0clsepcl  15794  sscoll2  15857