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  608  dn1dc  966  dfifp3dc  988  ifpdfbidc  991  xorbi2d  1422  dfbi3dc  1439  xordidc  1441  eleq2w  2291  eleq2  2293  ceqsex2  2841  ceqsex6v  2845  vtocl2gaf  2868  ceqsrex2v  2935  mob2  2983  eqreu  2995  nelrdva  3010  dfss4st  3437  undif4  3554  r19.27m  3587  ifbi  3623  preq12bg  3851  opeq2  3858  ralunsn  3876  intab  3952  disjiun  4078  brimralrspcev  4143  opabbid  4149  opthg  4324  pocl  4394  ordelord  4472  ordtriexmid  4613  ontr2exmid  4617  onsucsssucexmid  4619  tfisi  4679  xpeq2  4734  rabxp  4756  vtoclr  4767  opeliunxp  4774  posng  4791  opbrop  4798  rexiunxp  4864  elrnmpt1  4975  dfres2  5057  brcodir  5116  poltletr  5129  xp11m  5167  elxp4  5216  elxp5  5217  dffun4f  5334  fununi  5389  fneq2  5410  fnun  5429  feq3  5458  foeq3  5548  funfveu  5642  funbrfv  5672  ssimaexg  5698  fvopab3g  5709  fvopab3ig  5710  fvelrn  5768  fmptco  5803  fsn2  5811  elunirn  5896  isoeq2  5932  isoeq3  5933  isocnv2  5942  isoini  5948  isopolem  5952  f1oiso  5956  f1oiso2  5957  oprabbid  6063  cbvoprab3  6086  mpomptx  6101  mpofun  6112  ov  6130  ovi3  6148  ov6g  6149  ovg  6150  caoftrn  6257  uchoice  6289  f1o2ndf1  6380  xporderlem  6383  f1od2  6387  brtpos2  6403  brtposg  6406  dftpos4  6415  recseq  6458  tfrlem3-2d  6464  tfrlemi1  6484  tfrexlem  6486  tfr1onlemaccex  6500  tfrcllemaccex  6513  tfrcl  6516  freceq1  6544  freceq2  6545  frecsuc  6559  nnaordex  6682  brecop  6780  eroveu  6781  erovlem  6782  ecopovtrn  6787  ecopovtrng  6790  th3qlem1  6792  th3qlem2  6793  th3q  6795  elpmg  6819  ixpsnval  6856  ixpsnf1o  6891  domeng  6909  dom2lem  6931  xpcomco  6993  xpassen  6997  xpdom2  6998  xpf1o  7013  phplem3g  7025  ssfiexmid  7046  domfiexmid  7048  findcard2  7059  findcard2s  7060  findcard2d  7061  findcard2sd  7062  diffifi  7064  fiintim  7104  opabfi  7111  fidcenumlemrk  7132  fidcenumlemr  7133  supeq2  7167  nninfninc  7301  nnnninfeq2  7307  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  isacnm  7396  acfun  7400  2omotaplemap  7454  2omotaplemst  7455  exmidapne  7457  ccfunen  7461  recexnq  7588  recmulnqg  7589  ltsonq  7596  enq0sym  7630  enq0ref  7631  enq0tr  7632  enq0breq  7634  addnq0mo  7645  mulnq0mo  7646  addnnnq0  7647  mulnnnq0  7648  elinp  7672  prdisj  7690  prarloclem3  7695  prarloc  7701  distrlem5prl  7784  distrlem5pru  7785  ltexprlemell  7796  ltexprlemelu  7797  recexprlemm  7822  addsrmo  7941  mulsrmo  7942  addsrpr  7943  mulsrpr  7944  lttrsr  7960  recexgt0sr  7971  mulgt0sr  7976  ltresr  8037  axprecex  8078  axpre-lttrn  8082  axpre-mulgt0  8085  eqlelt  8244  lesub0  8637  apreap  8745  apreim  8761  aprcl  8804  aptap  8808  zltlen  9536  prime  9557  fzind  9573  qltlen  9847  xltnegi  10043  ixxval  10104  fzval  10218  fzdifsuc  10289  elfzm11  10299  elfzo  10357  zsupcllemex  10462  exbtwnzlemshrink  10480  rebtwn2zlemshrink  10485  facwordi  10974  zfz1iso  11076  pfxsuff1eqwrdeq  11246  wrd2ind  11270  shftfvalg  11344  shftfibg  11346  shftfval  11347  shftfib  11349  shftfn  11350  2shfti  11357  cau3lem  11640  caubnd2  11643  xrmaxiflemcom  11775  clim  11807  clim2  11809  climi  11813  climcn2  11835  addcn2  11836  subcn2  11837  mulcn2  11838  summodclem2a  11907  summodc  11909  fsum3  11913  fsumsplitf  11934  prodfdivap  12073  ntrivcvgap0  12075  prodeq1f  12078  prodeq2w  12082  prodeq2  12083  prodmodc  12104  zproddc  12105  fprodseq  12109  fprodntrivap  12110  fproddivapf  12157  fprodsplitf  12158  fprodsplit1f  12160  sinbnd  12278  cosbnd  12279  divalgb  12451  ndvdssub  12456  gcdval  12495  gcdneg  12518  bezoutlemstep  12533  bezoutlemmain  12534  bezoutlemex  12537  dfgcd2  12550  gcdass  12551  algcvgblem  12586  lcmval  12600  lcmneg  12611  lcmgcdlem  12614  lcmass  12622  qredeq  12633  prmind2  12657  euclemma  12683  pw2dvdslemn  12702  qnumval  12722  qdenval  12723  pceu  12833  pczpre  12835  pcdiv  12840  prmpwdvds  12893  prdsex  13317  gsumpropd  13440  gsumpropd2  13441  gsumress  13443  gsum0g  13444  mnd1  13503  grp1  13654  qusgrp2  13665  nmznsg  13765  releqgg  13772  eqgex  13773  iscmnd  13850  issrg  13943  iscrng2  13993  qusring2  14044  opprunitd  14089  crngunit  14090  dfrhm2  14133  rhmopp  14155  issubrng  14178  resrhm2b  14228  islmod  14270  lsssetm  14335  lsspropdg  14410  ixpsnbasval  14445  basis2  14737  eltg2  14742  isnei  14833  isneip  14835  restbasg  14857  iscnp  14888  iscnp3  14892  tgcn  14897  icnpimaex  14900  lmbrf  14904  cncnp  14919  cnptoprest2  14929  txbas  14947  txcnp  14960  imasnopn  14988  ispsmet  15012  ismet  15033  isxmet  15034  ismet2  15043  blres  15123  metcnp3  15200  txmetcnp  15207  mulcncf  15297  ellimc3apf  15349  limcdifap  15351  limcmpted  15352  limccnp2lem  15365  dvmptfsum  15414  elply2  15424  sincosq3sgn  15517  lgsquadlem1  15771  2sqlem8  15817  2sqlem9  15818  subctctexmid  16425  nnnninfex  16448