Theorem anbi2d 468

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  anbi2  471  anbi1cd  472  anbi12d  477  bi2anan9  614  dn1dc  973  dfifp3dc  995  ifpdfbidc  998  xorbi2d  1429  dfbi3dc  1446  xordidc  1448  eleq2w  2300  eleq2  2302  ceqsex2  2863  ceqsex6v  2867  vtocl2gaf  2890  ceqsrex2v  2958  mob2  3006  eqreu  3018  nelrdva  3033  dfss4st  3464  undif4  3587  r19.27m  3623  ifbi  3661  preq12bg  3898  opeq2  3905  ralunsn  3923  intab  3999  disjiun  4125  brimralrspcev  4191  opabbid  4197  opthg  4380  pocl  4450  ordelord  4528  ordtriexmid  4670  ontr2exmid  4674  onsucsssucexmid  4676  tfisi  4736  xpeq2  4791  rabxp  4814  vtoclr  4825  opeliunxp  4832  posng  4849  opbrop  4856  rexiunxp  4924  elrnmpt1  5035  dfres2  5118  brcodir  5178  poltletr  5191  xp11m  5229  elxp4  5278  elxp5  5279  dffun4f  5396  fununi  5452  fneq2  5473  fnun  5492  feq3  5521  foeq3  5616  funfveu  5711  funbrfv  5742  ssimaexg  5768  fvopab3g  5781  fvopab3ig  5782  fvelrn  5842  fmptco  5877  fsn2  5885  elunirn  5975  isoeq2  6011  isoeq3  6012  isocnv2  6021  isoini  6027  isopolem  6031  f1oiso  6035  f1oiso2  6036  oprabbid  6144  cbvoprab3  6167  mpomptx  6182  mpofun  6193  ov  6211  ovi3  6229  ov6g  6230  ovg  6231  caoftrn  6339  uchoice  6375  f1o2ndf1  6468  xporderlem  6471  f1od2  6475  suppimacnvfn  6490  brtpos2  6527  brtposg  6530  dftpos4  6539  recseq  6582  tfrlem3-2d  6588  tfrlemi1  6608  tfrexlem  6610  tfr1onlemaccex  6624  tfrcllemaccex  6637  tfrcl  6640  freceq1  6668  freceq2  6669  frecsuc  6683  nnaordex  6806  brecop  6904  eroveu  6905  erovlem  6906  ecopovtrn  6911  ecopovtrng  6914  th3qlem1  6916  th3qlem2  6917  th3q  6919  elpmg  6943  ixpsnval  6989  ixpsnf1o  7024  domeng  7042  dom2lem  7064  mapsnend  7105  modom  7114  xpcomco  7130  xpassen  7134  xpdom2  7135  xpf1o  7150  phplem3g  7163  ssfiexmid  7184  ssfiexmidt  7186  domfiexmid  7188  findcard2  7199  findcard2s  7200  findcard2d  7201  findcard2sd  7202  diffifi  7204  fiintim  7244  opabfi  7253  fidcenumlemrk  7278  fidcenumlemr  7279  supeq2  7335  nninfninc  7469  nnnninfeq2  7475  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  isacnm  7565  acfun  7569  2omotaplemap  7629  2omotaplemst  7630  exmidapne  7632  ccfunen  7636  recexnq  7763  recmulnqg  7764  ltsonq  7771  enq0sym  7805  enq0ref  7806  enq0tr  7807  enq0breq  7809  addnq0mo  7820  mulnq0mo  7821  addnnnq0  7822  mulnnnq0  7823  elinp  7847  prdisj  7865  prarloclem3  7870  prarloc  7876  distrlem5prl  7959  distrlem5pru  7960  ltexprlemell  7971  ltexprlemelu  7972  recexprlemm  7997  addsrmo  8116  mulsrmo  8117  addsrpr  8118  mulsrpr  8119  lttrsr  8135  recexgt0sr  8146  mulgt0sr  8151  ltresr  8212  axprecex  8253  axpre-lttrn  8257  axpre-mulgt0  8260  eqlelt  8418  lesub0  8814  apreap  8923  apreim  8939  aprcl  8982  aptap  8986  zltlen  9733  prime  9755  fzind  9771  qltlen  10055  xltnegi  10253  ixxval  10314  fzval  10429  fzdifsuc  10504  elfzm11  10514  elfzo  10572  zsupcllemex  10679  exbtwnzlemshrink  10699  rebtwn2zlemshrink  10704  facwordi  11199  zfz1iso  11314  pfxsuff1eqwrdeq  11492  wrd2ind  11516  shftfvalg  11604  shftfibg  11606  shftfval  11607  shftfib  11609  shftfn  11610  2shfti  11617  cau3lem  11902  caubnd2  11905  xrmaxiflemcom  12039  clim  12071  clim2  12073  climi  12077  climcn2  12099  addcn2  12100  subcn2  12101  mulcn2  12102  summodclem2a  12172  summodc  12174  fsum3  12178  fsumsplitf  12199  prodfdivap  12338  ntrivcvgap0  12340  prodeq1f  12343  prodeq2w  12347  prodeq2  12348  prodmodc  12369  zproddc  12370  fprodseq  12374  fprodntrivap  12375  fproddivapf  12422  fprodsplitf  12423  fprodsplit1f  12425  sinbnd  12543  cosbnd  12544  divalgb  12716  ndvdssub  12721  gcdval  12760  gcdneg  12783  bezoutlemstep  12798  bezoutlemmain  12799  bezoutlemex  12802  dfgcd2  12815  gcdass  12816  algcvgblem  12851  lcmval  12865  lcmneg  12876  lcmgcdlem  12879  lcmass  12887  qredeq  12898  prmind2  12922  euclemma  12949  pwbdvdslemn  12968  qnumval  12989  qdenval  12990  pceu  13102  pczpre  13104  pcdiv  13109  prmpwdvds  13162  gzsumress  13770  gzsum0  13771  mnd1  13820  grp1  13969  qusgrp2  13974  nmznsg  14074  releqgg  14081  eqgex  14082  resscntz  14165  iscmnd  14190  gsumvalfi  14241  prdsex  14278  issrg  14375  iscrng2  14425  qusring2  14479  opprunitd  14525  crngunit  14526  dfrhm2  14569  rhmopp  14591  issubrng  14615  resrhm2b  14665  islmod  14735  lsssetm  14801  lsspropdg  14876  ixpsnbasval  14911  basis2  15291  eltg2  15296  isnei  15387  isneip  15389  restbasg  15411  iscnp  15442  iscnp3  15446  tgcn  15451  icnpimaex  15454  lmbrf  15458  cncnp  15473  cnptoprest2  15483  txbas  15501  txcnp  15514  imasnopn  15542  ispsmet  15566  ismet  15587  isxmet  15588  ismet2  15597  blres  15677  metcnp3  15754  txmetcnp  15761  mulcncf  15851  ellimc3apf  15903  limcdifap  15905  limcmpted  15906  limccnp2lem  15919  dvmptfsum  15968  elply2  15978  sincosq3sgn  16072  zprmlogbaplem3  16234  pellexlem3  16248  lgsquadlem1  16418  2sqlem8  16464  2sqlem9  16465  eupthres  16920  eupth2lem3lem6fi  16934  subctctexmid  17252  wexmiddifxy  17268  nnnninfex  17288