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  964  xorbi1d  1401  drsb1  1823  ax11ev  1852  eleq1w  2267  eleq1  2269  rexeqf  2700  reueq1f  2701  rmoeq1f  2702  rabeqf  2763  vtocl2gaf  2842  alexeq  2903  ceqex  2904  elrabi  2930  sbc5  3026  rexss  3264  ineq1  3371  difin2  3439  r19.28m  3554  elif  3587  preq12bg  3820  opeq1  3825  eluni  3859  disjiun  4046  mpteq12f  4132  axsep2  4171  zfauscl  4172  opthg  4290  copsexg  4296  euotd  4307  elopab  4312  pocl  4358  uniuni  4506  rabxfrd  4524  ontr2exmid  4581  regexmidlemm  4588  regexmidlem1  4589  reg2exmidlema  4590  preleq  4611  xpeq1  4697  elxpi  4699  vtoclr  4731  opbrop  4762  opelresg  4975  resopab2  5015  elxp4  5179  elxp5  5180  cnvpom  5234  fun11  5350  feq2  5419  f1eq2  5489  f1eq3  5490  foeq2  5507  brprcneu  5582  ssimaexg  5654  dmfco  5660  fndmdif  5698  rexsupp  5717  respreima  5721  isoeq5  5887  isoini  5900  isopolem  5904  f1oiso  5908  f1oiso2  5909  riotaeqdv  5913  acexmidlemab  5951  acexmidlemcase  5952  oprabid  5989  mpoeq123  6017  mpoeq123dva  6019  eloprabga  6045  resoprab  6054  resoprab2  6055  ov  6078  ovi3  6096  ov6g  6097  ovg  6098  caoftrn  6204  opabex3d  6219  opabex3  6220  elxp7  6269  eloprabi  6295  cnvf1o  6324  xporderlem  6330  poxp  6331  smoel2  6402  frec0g  6496  freccllem  6501  frecfcllem  6503  frecsuclem  6505  frecsuc  6506  nnaordex  6627  qliftel  6715  brecop  6725  eroveu  6726  ecopovtrn  6732  ecopovtrng  6735  th3qlem2  6738  th3q  6740  ixpsnf1o  6836  dom2lem  6876  xpsnen  6931  xpassen  6940  pw2f1odclem  6946  xpf1o  6956  opabfi  7050  ctssdccl  7228  exmidapne  7392  dfplpq2  7487  dfmpq2  7488  ltsonq  7531  enq0sym  7565  enq0ref  7566  enq0tr  7567  enq0breq  7569  addnq0mo  7580  mulnq0mo  7581  addnnnq0  7582  mulnnnq0  7583  elinp  7607  prnmaxl  7621  prnminu  7622  prarloclemlo  7627  prarloc  7636  genpdflem  7640  genpassl  7657  genpassu  7658  ltexprlemm  7733  recexprlemell  7755  recexprlemelu  7756  cauappcvgprlemdisj  7784  caucvgprlemnkj  7799  caucvgprprlemnkltj  7822  caucvgprprlemnkeqj  7823  addsrmo  7876  mulsrmo  7877  addsrpr  7878  mulsrpr  7879  lttrsr  7895  mulgt0sr  7911  ltresr  7972  axpre-lttrn  8017  axpre-mulgt0  8020  recexgt0  8673  apreap  8680  apreim  8696  aprcl  8739  aptap  8743  prime  9492  rexuz  9721  ltxr  9917  ixxval  10038  fzval  10152  eqwrd  11056  pfxeq  11172  wrd2ind  11199  sqrtrval  11386  abslt  11474  absle  11475  lenegsq  11481  abs2difabs  11494  2clim  11687  climcn2  11695  addcn2  11696  mulcn2  11698  climrecvg1n  11734  sumeq1  11741  fsum2dlemstep  11820  modfsummod  11844  prodeq1f  11938  fprod2dlemstep  12008  nndivdvds  12182  divalg2  12312  gcdval  12355  bezoutlemstep  12393  bezoutlemmain  12394  bezoutlemex  12397  gcdass  12411  lcmval  12460  lcmass  12482  rpexp  12550  pythagtriplem2  12664  pythagtrip  12681  gsumfzval  13298  issgrpv  13311  issgrpn0  13312  ismhm  13368  mhmpropd  13373  issubm  13379  issubg  13584  issubg3  13603  ringpropd  13875  crngpropd  13876  opprunitd  13947  issubrg  14058  resrhm2b  14086  islmod  14128  lmodlema  14129  lmodprop2d  14185  islssm  14194  islssmg  14195  lsslss  14218  znleval  14490  psrbag  14506  istopg  14546  basis2  14595  tg2  14607  iscld  14650  neival  14690  isnei  14691  isneip  14693  iscn  14744  cnpval  14745  iscnp  14746  txbas  14805  txdis1cn  14825  ispsmet  14870  ismet  14891  isxmet  14892  ismet2  14901  blres  14981  elmopn  14993  mopni  15029  neibl  15038  metrest  15053  elcncf  15120  mulc1cncf  15136  mulcncf  15155  limccnp2lem  15223  sincosq2sgn  15374  sincosq4sgn  15376  2lgslem1a  15640  bdsep2  15960  bdzfauscl  15964  bj-d0clsepcl  15999  sscoll2  16062