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  610  dn1dc  969  dfifp3dc  991  ifpdfbidc  994  xorbi2d  1425  dfbi3dc  1442  xordidc  1444  eleq2w  2294  eleq2  2296  ceqsex2  2855  ceqsex6v  2859  vtocl2gaf  2882  ceqsrex2v  2949  mob2  2997  eqreu  3009  nelrdva  3024  dfss4st  3454  undif4  3571  r19.27m  3605  ifbi  3643  preq12bg  3877  opeq2  3884  ralunsn  3902  intab  3978  disjiun  4104  brimralrspcev  4169  opabbid  4175  opthg  4354  pocl  4424  ordelord  4502  ordtriexmid  4643  ontr2exmid  4647  onsucsssucexmid  4649  tfisi  4709  xpeq2  4764  rabxp  4787  vtoclr  4798  opeliunxp  4805  posng  4822  opbrop  4829  rexiunxp  4897  elrnmpt1  5008  dfres2  5090  brcodir  5150  poltletr  5163  xp11m  5201  elxp4  5250  elxp5  5251  dffun4f  5368  fununi  5424  fneq2  5445  fnun  5464  feq3  5493  foeq3  5588  funfveu  5683  funbrfv  5713  ssimaexg  5739  fvopab3g  5750  fvopab3ig  5751  fvelrn  5808  fmptco  5843  fsn2  5851  elunirn  5939  isoeq2  5975  isoeq3  5976  isocnv2  5985  isoini  5991  isopolem  5995  f1oiso  5999  f1oiso2  6000  oprabbid  6106  cbvoprab3  6129  mpomptx  6144  mpofun  6155  ov  6173  ovi3  6191  ov6g  6192  ovg  6193  caoftrn  6299  uchoice  6331  f1o2ndf1  6424  xporderlem  6427  f1od2  6431  suppimacnvfn  6446  brtpos2  6482  brtposg  6485  dftpos4  6494  recseq  6537  tfrlem3-2d  6543  tfrlemi1  6563  tfrexlem  6565  tfr1onlemaccex  6579  tfrcllemaccex  6592  tfrcl  6595  freceq1  6623  freceq2  6624  frecsuc  6638  nnaordex  6761  brecop  6859  eroveu  6860  erovlem  6861  ecopovtrn  6866  ecopovtrng  6869  th3qlem1  6871  th3qlem2  6872  th3q  6874  elpmg  6898  ixpsnval  6936  ixpsnf1o  6971  domeng  6989  dom2lem  7011  mapsnend  7052  modom  7061  xpcomco  7077  xpassen  7081  xpdom2  7082  xpf1o  7097  phplem3g  7110  ssfiexmid  7131  ssfiexmidt  7133  domfiexmid  7135  findcard2  7146  findcard2s  7147  findcard2d  7148  findcard2sd  7149  diffifi  7151  fiintim  7191  opabfi  7200  fidcenumlemrk  7224  fidcenumlemr  7225  supeq2  7280  nninfninc  7414  nnnninfeq2  7420  exmidfodomrlemr  7505  exmidfodomrlemrALT  7506  isacnm  7510  acfun  7514  2omotaplemap  7571  2omotaplemst  7572  exmidapne  7574  ccfunen  7578  recexnq  7705  recmulnqg  7706  ltsonq  7713  enq0sym  7747  enq0ref  7748  enq0tr  7749  enq0breq  7751  addnq0mo  7762  mulnq0mo  7763  addnnnq0  7764  mulnnnq0  7765  elinp  7789  prdisj  7807  prarloclem3  7812  prarloc  7818  distrlem5prl  7901  distrlem5pru  7902  ltexprlemell  7913  ltexprlemelu  7914  recexprlemm  7939  addsrmo  8058  mulsrmo  8059  addsrpr  8060  mulsrpr  8061  lttrsr  8077  recexgt0sr  8088  mulgt0sr  8093  ltresr  8154  axprecex  8195  axpre-lttrn  8199  axpre-mulgt0  8202  eqlelt  8360  lesub0  8753  apreap  8861  apreim  8877  aprcl  8920  aptap  8924  zltlen  9656  prime  9677  fzind  9693  qltlen  9972  xltnegi  10168  ixxval  10229  fzval  10344  fzdifsuc  10415  elfzm11  10425  elfzo  10483  zsupcllemex  10590  exbtwnzlemshrink  10608  rebtwn2zlemshrink  10613  facwordi  11102  zfz1iso  11213  pfxsuff1eqwrdeq  11391  wrd2ind  11415  shftfvalg  11503  shftfibg  11505  shftfval  11506  shftfib  11508  shftfn  11509  2shfti  11516  cau3lem  11799  caubnd2  11802  xrmaxiflemcom  11934  clim  11966  clim2  11968  climi  11972  climcn2  11994  addcn2  11995  subcn2  11996  mulcn2  11997  summodclem2a  12067  summodc  12069  fsum3  12073  fsumsplitf  12094  prodfdivap  12233  ntrivcvgap0  12235  prodeq1f  12238  prodeq2w  12242  prodeq2  12243  prodmodc  12264  zproddc  12265  fprodseq  12269  fprodntrivap  12270  fproddivapf  12317  fprodsplitf  12318  fprodsplit1f  12320  sinbnd  12438  cosbnd  12439  divalgb  12611  ndvdssub  12616  gcdval  12655  gcdneg  12678  bezoutlemstep  12693  bezoutlemmain  12694  bezoutlemex  12697  dfgcd2  12710  gcdass  12711  algcvgblem  12746  lcmval  12760  lcmneg  12771  lcmgcdlem  12774  lcmass  12782  qredeq  12793  prmind2  12817  euclemma  12843  pw2dvdslemn  12862  qnumval  12882  qdenval  12883  pceu  12993  pczpre  12995  pcdiv  13000  prmpwdvds  13053  prdsex  13482  gsumpropd  13605  gsumpropd2  13606  gsumress  13608  gsum0g  13609  mnd1  13668  grp1  13819  qusgrp2  13830  nmznsg  13930  releqgg  13937  eqgex  13938  iscmnd  14015  issrg  14109  iscrng2  14159  qusring2  14210  opprunitd  14255  crngunit  14256  dfrhm2  14299  rhmopp  14321  issubrng  14344  resrhm2b  14394  islmod  14439  lsssetm  14504  lsspropdg  14579  ixpsnbasval  14614  basis2  14913  eltg2  14918  isnei  15009  isneip  15011  restbasg  15033  iscnp  15064  iscnp3  15068  tgcn  15073  icnpimaex  15076  lmbrf  15080  cncnp  15095  cnptoprest2  15105  txbas  15123  txcnp  15136  imasnopn  15164  ispsmet  15188  ismet  15209  isxmet  15210  ismet2  15219  blres  15299  metcnp3  15376  txmetcnp  15383  mulcncf  15473  ellimc3apf  15525  limcdifap  15527  limcmpted  15528  limccnp2lem  15541  dvmptfsum  15590  elply2  15600  sincosq3sgn  15693  pellexlem3  15847  lgsquadlem1  15950  2sqlem8  15996  2sqlem9  15997  eupthres  16452  eupth2lem3lem6fi  16466  subctctexmid  16774  nnnninfex  16800  gfsumval  16862