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  2293  eleq2  2295  ceqsex2  2845  ceqsex6v  2849  vtocl2gaf  2872  ceqsrex2v  2939  mob2  2987  eqreu  2999  nelrdva  3014  dfss4st  3442  undif4  3559  r19.27m  3592  ifbi  3630  preq12bg  3861  opeq2  3868  ralunsn  3886  intab  3962  disjiun  4088  brimralrspcev  4153  opabbid  4159  opthg  4336  pocl  4406  ordelord  4484  ordtriexmid  4625  ontr2exmid  4629  onsucsssucexmid  4631  tfisi  4691  xpeq2  4746  rabxp  4769  vtoclr  4780  opeliunxp  4787  posng  4804  opbrop  4811  rexiunxp  4878  elrnmpt1  4989  dfres2  5071  brcodir  5131  poltletr  5144  xp11m  5182  elxp4  5231  elxp5  5232  dffun4f  5349  fununi  5405  fneq2  5426  fnun  5445  feq3  5474  foeq3  5566  funfveu  5661  funbrfv  5691  ssimaexg  5717  fvopab3g  5728  fvopab3ig  5729  fvelrn  5786  fmptco  5821  fsn2  5829  elunirn  5917  isoeq2  5953  isoeq3  5954  isocnv2  5963  isoini  5969  isopolem  5973  f1oiso  5977  f1oiso2  5978  oprabbid  6084  cbvoprab3  6107  mpomptx  6122  mpofun  6133  ov  6151  ovi3  6169  ov6g  6170  ovg  6171  caoftrn  6277  uchoice  6309  f1o2ndf1  6402  xporderlem  6405  f1od2  6409  suppimacnvfn  6424  brtpos2  6460  brtposg  6463  dftpos4  6472  recseq  6515  tfrlem3-2d  6521  tfrlemi1  6541  tfrexlem  6543  tfr1onlemaccex  6557  tfrcllemaccex  6570  tfrcl  6573  freceq1  6601  freceq2  6602  frecsuc  6616  nnaordex  6739  brecop  6837  eroveu  6838  erovlem  6839  ecopovtrn  6844  ecopovtrng  6847  th3qlem1  6849  th3qlem2  6850  th3q  6852  elpmg  6876  ixpsnval  6913  ixpsnf1o  6948  domeng  6966  dom2lem  6988  modom  7037  xpcomco  7053  xpassen  7057  xpdom2  7058  xpf1o  7073  phplem3g  7085  ssfiexmid  7106  ssfiexmidt  7108  domfiexmid  7110  findcard2  7121  findcard2s  7122  findcard2d  7123  findcard2sd  7124  diffifi  7126  fiintim  7166  opabfi  7175  fidcenumlemrk  7196  fidcenumlemr  7197  supeq2  7231  nninfninc  7365  nnnninfeq2  7371  exmidfodomrlemr  7456  exmidfodomrlemrALT  7457  isacnm  7461  acfun  7465  2omotaplemap  7519  2omotaplemst  7520  exmidapne  7522  ccfunen  7526  recexnq  7653  recmulnqg  7654  ltsonq  7661  enq0sym  7695  enq0ref  7696  enq0tr  7697  enq0breq  7699  addnq0mo  7710  mulnq0mo  7711  addnnnq0  7712  mulnnnq0  7713  elinp  7737  prdisj  7755  prarloclem3  7760  prarloc  7766  distrlem5prl  7849  distrlem5pru  7850  ltexprlemell  7861  ltexprlemelu  7862  recexprlemm  7887  addsrmo  8006  mulsrmo  8007  addsrpr  8008  mulsrpr  8009  lttrsr  8025  recexgt0sr  8036  mulgt0sr  8041  ltresr  8102  axprecex  8143  axpre-lttrn  8147  axpre-mulgt0  8150  eqlelt  8308  lesub0  8701  apreap  8809  apreim  8825  aprcl  8868  aptap  8872  zltlen  9602  prime  9623  fzind  9639  qltlen  9918  xltnegi  10114  ixxval  10175  fzval  10290  fzdifsuc  10361  elfzm11  10371  elfzo  10429  zsupcllemex  10536  exbtwnzlemshrink  10554  rebtwn2zlemshrink  10559  facwordi  11048  zfz1iso  11151  pfxsuff1eqwrdeq  11329  wrd2ind  11353  shftfvalg  11441  shftfibg  11443  shftfval  11444  shftfib  11446  shftfn  11447  2shfti  11454  cau3lem  11737  caubnd2  11740  xrmaxiflemcom  11872  clim  11904  clim2  11906  climi  11910  climcn2  11932  addcn2  11933  subcn2  11934  mulcn2  11935  summodclem2a  12005  summodc  12007  fsum3  12011  fsumsplitf  12032  prodfdivap  12171  ntrivcvgap0  12173  prodeq1f  12176  prodeq2w  12180  prodeq2  12181  prodmodc  12202  zproddc  12203  fprodseq  12207  fprodntrivap  12208  fproddivapf  12255  fprodsplitf  12256  fprodsplit1f  12258  sinbnd  12376  cosbnd  12377  divalgb  12549  ndvdssub  12554  gcdval  12593  gcdneg  12616  bezoutlemstep  12631  bezoutlemmain  12632  bezoutlemex  12635  dfgcd2  12648  gcdass  12649  algcvgblem  12684  lcmval  12698  lcmneg  12709  lcmgcdlem  12712  lcmass  12720  qredeq  12731  prmind2  12755  euclemma  12781  pw2dvdslemn  12800  qnumval  12820  qdenval  12821  pceu  12931  pczpre  12933  pcdiv  12938  prmpwdvds  12991  prdsex  13415  gsumpropd  13538  gsumpropd2  13539  gsumress  13541  gsum0g  13542  mnd1  13601  grp1  13752  qusgrp2  13763  nmznsg  13863  releqgg  13870  eqgex  13871  iscmnd  13948  issrg  14042  iscrng2  14092  qusring2  14143  opprunitd  14188  crngunit  14189  dfrhm2  14232  rhmopp  14254  issubrng  14277  resrhm2b  14327  islmod  14370  lsssetm  14435  lsspropdg  14510  ixpsnbasval  14545  basis2  14842  eltg2  14847  isnei  14938  isneip  14940  restbasg  14962  iscnp  14993  iscnp3  14997  tgcn  15002  icnpimaex  15005  lmbrf  15009  cncnp  15024  cnptoprest2  15034  txbas  15052  txcnp  15065  imasnopn  15093  ispsmet  15117  ismet  15138  isxmet  15139  ismet2  15148  blres  15228  metcnp3  15305  txmetcnp  15312  mulcncf  15402  ellimc3apf  15454  limcdifap  15456  limcmpted  15457  limccnp2lem  15470  dvmptfsum  15519  elply2  15529  sincosq3sgn  15622  pellexlem3  15776  lgsquadlem1  15879  2sqlem8  15925  2sqlem9  15926  eupthres  16381  eupth2lem3lem6fi  16395  subctctexmid  16705  nnnninfex  16731  gfsumval  16792