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  2842  ceqsex6v  2846  vtocl2gaf  2869  ceqsrex2v  2936  mob2  2984  eqreu  2996  nelrdva  3011  dfss4st  3438  undif4  3555  r19.27m  3588  ifbi  3624  preq12bg  3854  opeq2  3861  ralunsn  3879  intab  3955  disjiun  4081  brimralrspcev  4146  opabbid  4152  opthg  4328  pocl  4398  ordelord  4476  ordtriexmid  4617  ontr2exmid  4621  onsucsssucexmid  4623  tfisi  4683  xpeq2  4738  rabxp  4761  vtoclr  4772  opeliunxp  4779  posng  4796  opbrop  4803  rexiunxp  4870  elrnmpt1  4981  dfres2  5063  brcodir  5122  poltletr  5135  xp11m  5173  elxp4  5222  elxp5  5223  dffun4f  5340  fununi  5395  fneq2  5416  fnun  5435  feq3  5464  foeq3  5554  funfveu  5648  funbrfv  5678  ssimaexg  5704  fvopab3g  5715  fvopab3ig  5716  fvelrn  5774  fmptco  5809  fsn2  5817  elunirn  5902  isoeq2  5938  isoeq3  5939  isocnv2  5948  isoini  5954  isopolem  5958  f1oiso  5962  f1oiso2  5963  oprabbid  6069  cbvoprab3  6092  mpomptx  6107  mpofun  6118  ov  6136  ovi3  6154  ov6g  6155  ovg  6156  caoftrn  6263  uchoice  6295  f1o2ndf1  6388  xporderlem  6391  f1od2  6395  brtpos2  6412  brtposg  6415  dftpos4  6424  recseq  6467  tfrlem3-2d  6473  tfrlemi1  6493  tfrexlem  6495  tfr1onlemaccex  6509  tfrcllemaccex  6522  tfrcl  6525  freceq1  6553  freceq2  6554  frecsuc  6568  nnaordex  6691  brecop  6789  eroveu  6790  erovlem  6791  ecopovtrn  6796  ecopovtrng  6799  th3qlem1  6801  th3qlem2  6802  th3q  6804  elpmg  6828  ixpsnval  6865  ixpsnf1o  6900  domeng  6918  dom2lem  6940  modom  6989  xpcomco  7005  xpassen  7009  xpdom2  7010  xpf1o  7025  phplem3g  7037  ssfiexmid  7058  domfiexmid  7060  findcard2  7071  findcard2s  7072  findcard2d  7073  findcard2sd  7074  diffifi  7076  fiintim  7116  opabfi  7123  fidcenumlemrk  7144  fidcenumlemr  7145  supeq2  7179  nninfninc  7313  nnnninfeq2  7319  exmidfodomrlemr  7403  exmidfodomrlemrALT  7404  isacnm  7408  acfun  7412  2omotaplemap  7466  2omotaplemst  7467  exmidapne  7469  ccfunen  7473  recexnq  7600  recmulnqg  7601  ltsonq  7608  enq0sym  7642  enq0ref  7643  enq0tr  7644  enq0breq  7646  addnq0mo  7657  mulnq0mo  7658  addnnnq0  7659  mulnnnq0  7660  elinp  7684  prdisj  7702  prarloclem3  7707  prarloc  7713  distrlem5prl  7796  distrlem5pru  7797  ltexprlemell  7808  ltexprlemelu  7809  recexprlemm  7834  addsrmo  7953  mulsrmo  7954  addsrpr  7955  mulsrpr  7956  lttrsr  7972  recexgt0sr  7983  mulgt0sr  7988  ltresr  8049  axprecex  8090  axpre-lttrn  8094  axpre-mulgt0  8097  eqlelt  8256  lesub0  8649  apreap  8757  apreim  8773  aprcl  8816  aptap  8820  zltlen  9548  prime  9569  fzind  9585  qltlen  9864  xltnegi  10060  ixxval  10121  fzval  10235  fzdifsuc  10306  elfzm11  10316  elfzo  10374  zsupcllemex  10480  exbtwnzlemshrink  10498  rebtwn2zlemshrink  10503  facwordi  10992  zfz1iso  11095  pfxsuff1eqwrdeq  11270  wrd2ind  11294  shftfvalg  11369  shftfibg  11371  shftfval  11372  shftfib  11374  shftfn  11375  2shfti  11382  cau3lem  11665  caubnd2  11668  xrmaxiflemcom  11800  clim  11832  clim2  11834  climi  11838  climcn2  11860  addcn2  11861  subcn2  11862  mulcn2  11863  summodclem2a  11932  summodc  11934  fsum3  11938  fsumsplitf  11959  prodfdivap  12098  ntrivcvgap0  12100  prodeq1f  12103  prodeq2w  12107  prodeq2  12108  prodmodc  12129  zproddc  12130  fprodseq  12134  fprodntrivap  12135  fproddivapf  12182  fprodsplitf  12183  fprodsplit1f  12185  sinbnd  12303  cosbnd  12304  divalgb  12476  ndvdssub  12481  gcdval  12520  gcdneg  12543  bezoutlemstep  12558  bezoutlemmain  12559  bezoutlemex  12562  dfgcd2  12575  gcdass  12576  algcvgblem  12611  lcmval  12625  lcmneg  12636  lcmgcdlem  12639  lcmass  12647  qredeq  12658  prmind2  12682  euclemma  12708  pw2dvdslemn  12727  qnumval  12747  qdenval  12748  pceu  12858  pczpre  12860  pcdiv  12865  prmpwdvds  12918  prdsex  13342  gsumpropd  13465  gsumpropd2  13466  gsumress  13468  gsum0g  13469  mnd1  13528  grp1  13679  qusgrp2  13690  nmznsg  13790  releqgg  13797  eqgex  13798  iscmnd  13875  issrg  13968  iscrng2  14018  qusring2  14069  opprunitd  14114  crngunit  14115  dfrhm2  14158  rhmopp  14180  issubrng  14203  resrhm2b  14253  islmod  14295  lsssetm  14360  lsspropdg  14435  ixpsnbasval  14470  basis2  14762  eltg2  14767  isnei  14858  isneip  14860  restbasg  14882  iscnp  14913  iscnp3  14917  tgcn  14922  icnpimaex  14925  lmbrf  14929  cncnp  14944  cnptoprest2  14954  txbas  14972  txcnp  14985  imasnopn  15013  ispsmet  15037  ismet  15058  isxmet  15059  ismet2  15068  blres  15148  metcnp3  15225  txmetcnp  15232  mulcncf  15322  ellimc3apf  15374  limcdifap  15376  limcmpted  15377  limccnp2lem  15390  dvmptfsum  15439  elply2  15449  sincosq3sgn  15542  lgsquadlem1  15796  2sqlem8  15842  2sqlem9  15843  eupthres  16252  subctctexmid  16537  nnnninfex  16560