Theorem anbi1d 469

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  anbi1  470  anbi12d  477  bi2anan9  614  pm5.71dc  974  dfifp4dc  996  dfifp5dc  997  xorbi1d  1430  drsb1  1852  ax11ev  1881  eleq1w  2299  eleq1  2301  rexeqf  2746  reueq1f  2747  rmoeq1f  2748  rabeqf  2811  vtocl2gaf  2890  alexeq  2952  ceqex  2953  elrabi  2979  sbc5  3075  rexss  3315  ineq1  3425  difin2  3493  r19.28m  3617  elif  3652  ifeqeqxdc  3687  rabsnifsb  3777  preq12bg  3898  opeq1  3904  eluni  3938  disjiun  4125  mpteq12f  4212  axsepg  4252  sepg  4253  zfausclOLD  4255  opthg  4380  copsexg  4386  euotd  4397  elopab  4402  pocl  4450  uniuni  4599  rabxfrd  4617  ontr2exmid  4674  regexmidlemm  4681  regexmidlem1  4682  reg2exmidlema  4683  preleq  4704  xpeq1  4790  elxpi  4792  vtoclr  4825  opbrop  4856  opelresg  5072  resopab2  5113  elxp4  5278  elxp5  5279  cnvpom  5333  fun11  5451  feq2  5520  f1eq2  5597  f1eq3  5598  foeq2  5615  brprcneu  5691  ssimaexg  5768  dmfco  5776  fndmdif  5817  respreima  5839  isoeq5  6014  isoini  6027  isopolem  6031  f1oiso  6035  f1oiso2  6036  riotaeqdv  6042  acexmidlemab  6082  acexmidlemcase  6083  oprabid  6120  mpoeq123  6150  mpoeq123dva  6152  eloprabga  6178  resoprab  6187  resoprab2  6188  ov  6211  ovi3  6229  ov6g  6230  ovg  6231  caoftrn  6339  opabex3d  6354  opabex3  6355  elxp7  6408  eloprabi  6436  cnvf1o  6465  xporderlem  6471  poxp  6472  rexsupp  6497  smoel2  6579  frec0g  6673  freccllem  6678  frecfcllem  6680  frecsuclem  6682  frecsuc  6683  nnaordex  6806  qliftel  6894  brecop  6904  eroveu  6905  ecopovtrn  6911  ecopovtrng  6914  th3qlem2  6917  th3q  6919  ixpsnf1o  7024  dom2lem  7064  mapsnend  7105  modom  7114  xpsnen  7125  xpassen  7134  pw2f1odclem  7140  xpf1o  7150  opabfi  7253  ctssdccl  7457  exmidapne  7632  dfplpq2  7727  dfmpq2  7728  ltsonq  7771  enq0sym  7805  enq0ref  7806  enq0tr  7807  enq0breq  7809  addnq0mo  7820  mulnq0mo  7821  addnnnq0  7822  mulnnnq0  7823  elinp  7847  prnmaxl  7861  prnminu  7862  prarloclemlo  7867  prarloc  7876  genpdflem  7880  genpassl  7897  genpassu  7898  ltexprlemm  7973  recexprlemell  7995  recexprlemelu  7996  cauappcvgprlemdisj  8024  caucvgprlemnkj  8039  caucvgprprlemnkltj  8062  caucvgprprlemnkeqj  8063  addsrmo  8116  mulsrmo  8117  addsrpr  8118  mulsrpr  8119  lttrsr  8135  mulgt0sr  8151  ltresr  8212  axpre-lttrn  8257  axpre-mulgt0  8260  recexgt0  8916  apreap  8923  apreim  8939  aprcl  8982  aptap  8986  prime  9755  rexuz  9995  ltxr  10193  ixxval  10314  fzval  10429  hashfibclem  11303  hashf1lem2  11307  eqwrd  11366  pfxeq  11489  wrd2ind  11516  sqrtrval  11787  abslt  11876  absle  11877  lenegsq  11883  abs2difabs  11896  2clim  12091  climcn2  12099  addcn2  12100  mulcn2  12102  climrecvg1n  12138  sumeq1  12145  fsum2dlemstep  12225  modfsummod  12249  prodeq1f  12343  fprod2dlemstep  12413  nndivdvds  12587  divalg2  12717  gcdval  12760  bezoutlemstep  12798  bezoutlemmain  12799  bezoutlemex  12802  gcdass  12816  lcmval  12865  lcmass  12887  rpexp  12956  pythagtriplem2  13073  pythagtrip  13090  gzsumfzval  13769  issgrpv  13777  issgrpn0  13778  ismhm  13826  mhmpropd  13831  issubm  13837  issubg  14034  issubg3  14053  ringpropd  14449  crngpropd  14450  opprunitd  14525  issubrg  14637  resrhm2b  14665  islmod  14735  lmodlema  14736  lmodprop2d  14793  islssm  14802  islssmg  14803  lsslss  14826  znleval  15096  psrbag  15163  istopg  15242  basis2  15291  tg2  15303  iscld  15346  neival  15386  isnei  15387  isneip  15389  iscn  15440  cnpval  15441  iscnp  15442  txbas  15501  txdis1cn  15521  ispsmet  15566  ismet  15587  isxmet  15588  ismet2  15597  blres  15677  elmopn  15689  mopni  15725  neibl  15734  metrest  15749  elcncf  15816  mulc1cncf  15832  mulcncf  15851  limccnp2lem  15919  sincosq2sgn  16071  sincosq4sgn  16073  pellexlem3  16248  bpos  16337  2lgslem1a  16429  edgssv2en  16662  uhgr2edg  16669  vtxdfifiun  16760  trlsfvalg  16846  istrl  16848  clwwlknp  16880  iseupth  16910  eupth2lem2dc  16922  bdsep2  17134  bdsepg  17138  bj-d0clsepcl  17173  sscoll2  17236  wexmiddifxy  17268