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  962  xorbi2d  1391  dfbi3dc  1408  xordidc  1410  eleq2w  2255  eleq2  2257  ceqsex2  2801  ceqsex6v  2805  vtocl2gaf  2828  ceqsrex2v  2893  mob2  2941  eqreu  2953  nelrdva  2968  dfss4st  3393  undif4  3510  r19.27m  3543  ifbi  3578  preq12bg  3800  opeq2  3806  ralunsn  3824  intab  3900  disjiun  4025  brimralrspcev  4089  opabbid  4095  opthg  4268  pocl  4335  ordelord  4413  ordtriexmid  4554  ontr2exmid  4558  onsucsssucexmid  4560  tfisi  4620  xpeq2  4675  rabxp  4697  vtoclr  4708  opeliunxp  4715  posng  4732  opbrop  4739  rexiunxp  4805  elrnmpt1  4914  dfres2  4995  brcodir  5054  poltletr  5067  xp11m  5105  elxp4  5154  elxp5  5155  dffun4f  5271  fununi  5323  fneq2  5344  fnun  5361  feq3  5389  foeq3  5475  funfveu  5568  funbrfv  5596  ssimaexg  5620  fvopab3g  5631  fvopab3ig  5632  fvelrn  5690  fmptco  5725  fsn2  5733  elunirn  5810  isoeq2  5846  isoeq3  5847  isocnv2  5856  isoini  5862  isopolem  5866  f1oiso  5870  f1oiso2  5871  oprabbid  5972  cbvoprab3  5995  mpomptx  6010  mpofun  6021  ov  6039  ovi3  6057  ov6g  6058  ovg  6059  caoftrn  6160  uchoice  6192  f1o2ndf1  6283  xporderlem  6286  f1od2  6290  brtpos2  6306  brtposg  6309  dftpos4  6318  recseq  6361  tfrlem3-2d  6367  tfrlemi1  6387  tfrexlem  6389  tfr1onlemaccex  6403  tfrcllemaccex  6416  tfrcl  6419  freceq1  6447  freceq2  6448  frecsuc  6462  nnaordex  6583  brecop  6681  eroveu  6682  erovlem  6683  ecopovtrn  6688  ecopovtrng  6691  th3qlem1  6693  th3qlem2  6694  th3q  6696  elpmg  6720  ixpsnval  6757  ixpsnf1o  6792  domeng  6808  dom2lem  6828  xpcomco  6882  xpassen  6886  xpdom2  6887  xpf1o  6902  phplem3g  6914  ssfiexmid  6934  domfiexmid  6936  findcard2  6947  findcard2s  6948  findcard2d  6949  findcard2sd  6950  diffifi  6952  fiintim  6987  opabfi  6994  fidcenumlemrk  7015  fidcenumlemr  7016  supeq2  7050  nninfninc  7184  nnnninfeq2  7190  exmidfodomrlemr  7264  exmidfodomrlemrALT  7265  acfun  7269  2omotaplemap  7319  2omotaplemst  7320  exmidapne  7322  ccfunen  7326  recexnq  7452  recmulnqg  7453  ltsonq  7460  enq0sym  7494  enq0ref  7495  enq0tr  7496  enq0breq  7498  addnq0mo  7509  mulnq0mo  7510  addnnnq0  7511  mulnnnq0  7512  elinp  7536  prdisj  7554  prarloclem3  7559  prarloc  7565  distrlem5prl  7648  distrlem5pru  7649  ltexprlemell  7660  ltexprlemelu  7661  recexprlemm  7686  addsrmo  7805  mulsrmo  7806  addsrpr  7807  mulsrpr  7808  lttrsr  7824  recexgt0sr  7835  mulgt0sr  7840  ltresr  7901  axprecex  7942  axpre-lttrn  7946  axpre-mulgt0  7949  eqlelt  8108  lesub0  8500  apreap  8608  apreim  8624  aprcl  8667  aptap  8671  zltlen  9398  prime  9419  fzind  9435  qltlen  9708  xltnegi  9904  ixxval  9965  fzval  10079  fzdifsuc  10150  elfzm11  10160  elfzo  10218  exbtwnzlemshrink  10320  rebtwn2zlemshrink  10325  facwordi  10814  zfz1iso  10915  shftfvalg  10965  shftfibg  10967  shftfval  10968  shftfib  10970  shftfn  10971  2shfti  10978  cau3lem  11261  caubnd2  11264  xrmaxiflemcom  11395  clim  11427  clim2  11429  climi  11433  climcn2  11455  addcn2  11456  subcn2  11457  mulcn2  11458  summodclem2a  11527  summodc  11529  fsum3  11533  fsumsplitf  11554  prodfdivap  11693  ntrivcvgap0  11695  prodeq1f  11698  prodeq2w  11702  prodeq2  11703  prodmodc  11724  zproddc  11725  fprodseq  11729  fprodntrivap  11730  fproddivapf  11777  fprodsplitf  11778  fprodsplit1f  11780  sinbnd  11898  cosbnd  11899  divalgb  12069  ndvdssub  12074  zsupcllemex  12086  gcdval  12099  gcdneg  12122  bezoutlemstep  12137  bezoutlemmain  12138  bezoutlemex  12141  dfgcd2  12154  gcdass  12155  algcvgblem  12190  lcmval  12204  lcmneg  12215  lcmgcdlem  12218  lcmass  12226  qredeq  12237  prmind2  12261  euclemma  12287  pw2dvdslemn  12306  qnumval  12326  qdenval  12327  pceu  12436  pczpre  12438  pcdiv  12443  prmpwdvds  12496  prdsex  12883  gsumpropd  12978  gsumpropd2  12979  gsumress  12981  gsum0g  12982  mnd1  13030  grp1  13181  qusgrp2  13186  nmznsg  13286  releqgg  13293  eqgex  13294  iscmnd  13371  issrg  13464  iscrng2  13514  qusring2  13565  opprunitd  13609  crngunit  13610  dfrhm2  13653  rhmopp  13675  issubrng  13698  resrhm2b  13748  islmod  13790  lsssetm  13855  lsspropdg  13930  ixpsnbasval  13965  basis2  14227  eltg2  14232  isnei  14323  isneip  14325  restbasg  14347  iscnp  14378  iscnp3  14382  tgcn  14387  icnpimaex  14390  lmbrf  14394  cncnp  14409  cnptoprest2  14419  txbas  14437  txcnp  14450  imasnopn  14478  ispsmet  14502  ismet  14523  isxmet  14524  ismet2  14533  blres  14613  metcnp3  14690  txmetcnp  14697  mulcncf  14787  ellimc3apf  14839  limcdifap  14841  limcmpted  14842  limccnp2lem  14855  dvmptfsum  14904  elply2  14914  sincosq3sgn  15004  lgsquadlem1  15234  2sqlem8  15280  2sqlem9  15281  subctctexmid  15561