Theorem anbi2d 464

Description: Deduction adding a left 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
anbi2d	⊢ (𝜑 → ((𝜃 ∧ 𝜓) ↔ (𝜃 ∧ 𝜒)))

Proof of Theorem anbi2d

Step	Hyp	Ref	Expression
1		anbid.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	a1d 22	. 2 ⊢ (𝜑 → (𝜃 → (𝜓 ↔ 𝜒)))
3	2	pm5.32d 450	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:  anbi2  467  anbi1cd  468  anbi12d  473  bi2anan9  606  dn1dc  963  xorbi2d  1400  dfbi3dc  1417  xordidc  1419  eleq2w  2268  eleq2  2270  ceqsex2  2815  ceqsex6v  2819  vtocl2gaf  2842  ceqsrex2v  2909  mob2  2957  eqreu  2969  nelrdva  2984  dfss4st  3410  undif4  3527  r19.27m  3560  ifbi  3595  preq12bg  3819  opeq2  3825  ralunsn  3843  intab  3919  disjiun  4045  brimralrspcev  4110  opabbid  4116  opthg  4289  pocl  4357  ordelord  4435  ordtriexmid  4576  ontr2exmid  4580  onsucsssucexmid  4582  tfisi  4642  xpeq2  4697  rabxp  4719  vtoclr  4730  opeliunxp  4737  posng  4754  opbrop  4761  rexiunxp  4827  elrnmpt1  4937  dfres2  5019  brcodir  5078  poltletr  5091  xp11m  5129  elxp4  5178  elxp5  5179  dffun4f  5295  fununi  5350  fneq2  5371  fnun  5390  feq3  5419  foeq3  5507  funfveu  5601  funbrfv  5629  ssimaexg  5653  fvopab3g  5664  fvopab3ig  5665  fvelrn  5723  fmptco  5758  fsn2  5766  elunirn  5847  isoeq2  5883  isoeq3  5884  isocnv2  5893  isoini  5899  isopolem  5903  f1oiso  5907  f1oiso2  5908  oprabbid  6010  cbvoprab3  6033  mpomptx  6048  mpofun  6059  ov  6077  ovi3  6095  ov6g  6096  ovg  6097  caoftrn  6203  uchoice  6235  f1o2ndf1  6326  xporderlem  6329  f1od2  6333  brtpos2  6349  brtposg  6352  dftpos4  6361  recseq  6404  tfrlem3-2d  6410  tfrlemi1  6430  tfrexlem  6432  tfr1onlemaccex  6446  tfrcllemaccex  6459  tfrcl  6462  freceq1  6490  freceq2  6491  frecsuc  6505  nnaordex  6626  brecop  6724  eroveu  6725  erovlem  6726  ecopovtrn  6731  ecopovtrng  6734  th3qlem1  6736  th3qlem2  6737  th3q  6739  elpmg  6763  ixpsnval  6800  ixpsnf1o  6835  domeng  6853  dom2lem  6875  xpcomco  6935  xpassen  6939  xpdom2  6940  xpf1o  6955  phplem3g  6967  ssfiexmid  6987  domfiexmid  6989  findcard2  7000  findcard2s  7001  findcard2d  7002  findcard2sd  7003  diffifi  7005  fiintim  7042  opabfi  7049  fidcenumlemrk  7070  fidcenumlemr  7071  supeq2  7105  nninfninc  7239  nnnninfeq2  7245  exmidfodomrlemr  7325  exmidfodomrlemrALT  7326  isacnm  7330  acfun  7334  2omotaplemap  7384  2omotaplemst  7385  exmidapne  7387  ccfunen  7391  recexnq  7518  recmulnqg  7519  ltsonq  7526  enq0sym  7560  enq0ref  7561  enq0tr  7562  enq0breq  7564  addnq0mo  7575  mulnq0mo  7576  addnnnq0  7577  mulnnnq0  7578  elinp  7602  prdisj  7620  prarloclem3  7625  prarloc  7631  distrlem5prl  7714  distrlem5pru  7715  ltexprlemell  7726  ltexprlemelu  7727  recexprlemm  7752  addsrmo  7871  mulsrmo  7872  addsrpr  7873  mulsrpr  7874  lttrsr  7890  recexgt0sr  7901  mulgt0sr  7906  ltresr  7967  axprecex  8008  axpre-lttrn  8012  axpre-mulgt0  8015  eqlelt  8174  lesub0  8567  apreap  8675  apreim  8691  aprcl  8734  aptap  8738  zltlen  9466  prime  9487  fzind  9503  qltlen  9776  xltnegi  9972  ixxval  10033  fzval  10147  fzdifsuc  10218  elfzm11  10228  elfzo  10286  zsupcllemex  10390  exbtwnzlemshrink  10408  rebtwn2zlemshrink  10413  facwordi  10902  zfz1iso  11003  pfxsuff1eqwrdeq  11170  wrd2ind  11194  shftfvalg  11199  shftfibg  11201  shftfval  11202  shftfib  11204  shftfn  11205  2shfti  11212  cau3lem  11495  caubnd2  11498  xrmaxiflemcom  11630  clim  11662  clim2  11664  climi  11668  climcn2  11690  addcn2  11691  subcn2  11692  mulcn2  11693  summodclem2a  11762  summodc  11764  fsum3  11768  fsumsplitf  11789  prodfdivap  11928  ntrivcvgap0  11930  prodeq1f  11933  prodeq2w  11937  prodeq2  11938  prodmodc  11959  zproddc  11960  fprodseq  11964  fprodntrivap  11965  fproddivapf  12012  fprodsplitf  12013  fprodsplit1f  12015  sinbnd  12133  cosbnd  12134  divalgb  12306  ndvdssub  12311  gcdval  12350  gcdneg  12373  bezoutlemstep  12388  bezoutlemmain  12389  bezoutlemex  12392  dfgcd2  12405  gcdass  12406  algcvgblem  12441  lcmval  12455  lcmneg  12466  lcmgcdlem  12469  lcmass  12477  qredeq  12488  prmind2  12512  euclemma  12538  pw2dvdslemn  12557  qnumval  12577  qdenval  12578  pceu  12688  pczpre  12690  pcdiv  12695  prmpwdvds  12748  prdsex  13171  gsumpropd  13294  gsumpropd2  13295  gsumress  13297  gsum0g  13298  mnd1  13357  grp1  13508  qusgrp2  13519  nmznsg  13619  releqgg  13626  eqgex  13627  iscmnd  13704  issrg  13797  iscrng2  13847  qusring2  13898  opprunitd  13942  crngunit  13943  dfrhm2  13986  rhmopp  14008  issubrng  14031  resrhm2b  14081  islmod  14123  lsssetm  14188  lsspropdg  14263  ixpsnbasval  14298  basis2  14590  eltg2  14595  isnei  14686  isneip  14688  restbasg  14710  iscnp  14741  iscnp3  14745  tgcn  14750  icnpimaex  14753  lmbrf  14757  cncnp  14772  cnptoprest2  14782  txbas  14800  txcnp  14813  imasnopn  14841  ispsmet  14865  ismet  14886  isxmet  14887  ismet2  14896  blres  14976  metcnp3  15053  txmetcnp  15060  mulcncf  15150  ellimc3apf  15202  limcdifap  15204  limcmpted  15205  limccnp2lem  15218  dvmptfsum  15267  elply2  15277  sincosq3sgn  15370  lgsquadlem1  15624  2sqlem8  15670  2sqlem9  15671  subctctexmid  16072  nnnninfex  16094