Theorem anbi2d 455

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 441	1 ⊢ (𝜑 → ((𝜃 ∧ 𝜓) ↔ (𝜃 ∧ 𝜒)))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  anbi2  458  anbi12d  460  bi2anan9  576  dn1dc  912  xorbi2d  1326  dfbi3dc  1343  xordidc  1345  eleq2w  2161  eleq2  2163  ceqsex2  2681  ceqsex6v  2685  vtocl2gaf  2708  ceqsrex2v  2771  mob2  2817  eqreu  2829  nelrdva  2844  dfss4st  3256  undif4  3372  r19.27m  3405  ifbi  3439  preq12bg  3647  opeq2  3653  ralunsn  3671  intab  3747  disjiun  3870  opabbid  3933  opthg  4098  pocl  4163  ordelord  4241  ordtriexmid  4375  ontr2exmid  4378  onsucsssucexmid  4380  tfisi  4439  xpeq2  4492  rabxp  4514  vtoclr  4525  opeliunxp  4532  posng  4549  opbrop  4556  rexiunxp  4619  elrnmpt1  4728  dfres2  4807  brcodir  4862  poltletr  4875  xp11m  4913  elxp4  4962  elxp5  4963  dffun4f  5075  fununi  5127  fneq2  5148  fnun  5165  feq3  5193  foeq3  5279  funfveu  5366  funbrfv  5392  ssimaexg  5415  fvopab3g  5426  fvopab3ig  5427  fvelrn  5483  fmptco  5518  fsn2  5526  elunirn  5599  isoeq2  5635  isoeq3  5636  isocnv2  5645  isoini  5651  isopolem  5655  f1oiso  5659  f1oiso2  5660  oprabbid  5756  cbvoprab3  5779  mpomptx  5794  mpofun  5805  ov  5822  ovi3  5839  ov6g  5840  ovg  5841  caoftrn  5938  f1o2ndf1  6055  xporderlem  6058  f1od2  6062  brtpos2  6078  brtposg  6081  dftpos4  6090  recseq  6133  tfrlem3-2d  6139  tfrlemi1  6159  tfrexlem  6161  tfr1onlemaccex  6175  tfrcllemaccex  6188  tfrcl  6191  freceq1  6219  freceq2  6220  frecsuc  6234  nnaordex  6353  brecop  6449  eroveu  6450  erovlem  6451  ecopovtrn  6456  ecopovtrng  6459  th3qlem1  6461  th3qlem2  6462  th3q  6464  elpmg  6488  ixpsnval  6525  ixpsnf1o  6560  domeng  6576  dom2lem  6596  xpcomco  6649  xpassen  6653  xpdom2  6654  xpf1o  6667  phplem3g  6679  ssfiexmid  6699  domfiexmid  6701  findcard2  6712  findcard2s  6713  findcard2d  6714  findcard2sd  6715  diffifi  6717  fiintim  6746  fidcenumlemrk  6770  fidcenumlemr  6771  supeq2  6791  exmidfodomrlemr  6967  exmidfodomrlemrALT  6968  recexnq  7099  recmulnqg  7100  ltsonq  7107  enq0sym  7141  enq0ref  7142  enq0tr  7143  enq0breq  7145  addnq0mo  7156  mulnq0mo  7157  addnnnq0  7158  mulnnnq0  7159  elinp  7183  prdisj  7201  prarloclem3  7206  prarloc  7212  distrlem5prl  7295  distrlem5pru  7296  ltexprlemell  7307  ltexprlemelu  7308  recexprlemm  7333  addsrmo  7439  mulsrmo  7440  addsrpr  7441  mulsrpr  7442  lttrsr  7458  recexgt0sr  7469  mulgt0sr  7473  ltresr  7526  axprecex  7565  axpre-lttrn  7569  axpre-mulgt0  7572  lesub0  8108  apreap  8215  apreim  8231  zltlen  8981  prime  9002  fzind  9018  qltlen  9282  xltnegi  9459  ixxval  9520  fzval  9633  fzdifsuc  9702  elfzm11  9712  elfzo  9767  exbtwnzlemshrink  9867  rebtwn2zlemshrink  9872  facwordi  10327  zfz1iso  10425  shftfvalg  10431  shftfibg  10433  shftfval  10434  shftfib  10436  shftfn  10437  2shfti  10444  cau3lem  10726  caubnd2  10729  xrmaxiflemcom  10857  clim  10889  clim2  10891  climi  10895  climcn2  10917  addcn2  10918  subcn2  10919  mulcn2  10920  summodclem2a  10989  summodc  10991  fsum3  10995  fsumsplitf  11016  sinbnd  11257  cosbnd  11258  divalgb  11417  ndvdssub  11422  zsupcllemex  11434  gcdval  11443  gcdneg  11465  bezoutlemstep  11478  bezoutlemmain  11479  bezoutlemex  11482  dfgcd2  11495  gcdass  11496  algcvgblem  11523  lcmval  11537  lcmneg  11548  lcmgcdlem  11551  lcmass  11559  qredeq  11570  prmind2  11594  euclemma  11617  pw2dvdslemn  11635  qnumval  11655  qdenval  11656  basis2  11997  eltg2  12004  isnei  12095  isneip  12097  restbasg  12119  iscnp  12149  iscnp3  12153  tgcn  12158  icnpimaex  12161  lmbrf  12165  cncnp  12180  cnptoprest2  12190  txbas  12208  txcnp  12221  imasnopn  12249  ispsmet  12251  ismet  12272  isxmet  12273  ismet2  12282  blres  12362  metcnp3  12435  mulcncf  12503  ellimc3ap  12511  limcdifap  12512