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  968  dfifp3dc  990  ifpdfbidc  993  xorbi2d  1424  dfbi3dc  1441  xordidc  1443  eleq2w  2293  eleq2  2295  ceqsex2  2844  ceqsex6v  2848  vtocl2gaf  2871  ceqsrex2v  2938  mob2  2986  eqreu  2998  nelrdva  3013  dfss4st  3440  undif4  3557  r19.27m  3590  ifbi  3626  preq12bg  3856  opeq2  3863  ralunsn  3881  intab  3957  disjiun  4083  brimralrspcev  4148  opabbid  4154  opthg  4330  pocl  4400  ordelord  4478  ordtriexmid  4619  ontr2exmid  4623  onsucsssucexmid  4625  tfisi  4685  xpeq2  4740  rabxp  4763  vtoclr  4774  opeliunxp  4781  posng  4798  opbrop  4805  rexiunxp  4872  elrnmpt1  4983  dfres2  5065  brcodir  5124  poltletr  5137  xp11m  5175  elxp4  5224  elxp5  5225  dffun4f  5342  fununi  5398  fneq2  5419  fnun  5438  feq3  5467  foeq3  5557  funfveu  5652  funbrfv  5682  ssimaexg  5708  fvopab3g  5719  fvopab3ig  5720  fvelrn  5778  fmptco  5813  fsn2  5821  elunirn  5907  isoeq2  5943  isoeq3  5944  isocnv2  5953  isoini  5959  isopolem  5963  f1oiso  5967  f1oiso2  5968  oprabbid  6074  cbvoprab3  6097  mpomptx  6112  mpofun  6123  ov  6141  ovi3  6159  ov6g  6160  ovg  6161  caoftrn  6268  uchoice  6300  f1o2ndf1  6393  xporderlem  6396  f1od2  6400  brtpos2  6417  brtposg  6420  dftpos4  6429  recseq  6472  tfrlem3-2d  6478  tfrlemi1  6498  tfrexlem  6500  tfr1onlemaccex  6514  tfrcllemaccex  6527  tfrcl  6530  freceq1  6558  freceq2  6559  frecsuc  6573  nnaordex  6696  brecop  6794  eroveu  6795  erovlem  6796  ecopovtrn  6801  ecopovtrng  6804  th3qlem1  6806  th3qlem2  6807  th3q  6809  elpmg  6833  ixpsnval  6870  ixpsnf1o  6905  domeng  6923  dom2lem  6945  modom  6994  xpcomco  7010  xpassen  7014  xpdom2  7015  xpf1o  7030  phplem3g  7042  ssfiexmid  7063  ssfiexmidt  7065  domfiexmid  7067  findcard2  7078  findcard2s  7079  findcard2d  7080  findcard2sd  7081  diffifi  7083  fiintim  7123  opabfi  7132  fidcenumlemrk  7153  fidcenumlemr  7154  supeq2  7188  nninfninc  7322  nnnninfeq2  7328  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  isacnm  7418  acfun  7422  2omotaplemap  7476  2omotaplemst  7477  exmidapne  7479  ccfunen  7483  recexnq  7610  recmulnqg  7611  ltsonq  7618  enq0sym  7652  enq0ref  7653  enq0tr  7654  enq0breq  7656  addnq0mo  7667  mulnq0mo  7668  addnnnq0  7669  mulnnnq0  7670  elinp  7694  prdisj  7712  prarloclem3  7717  prarloc  7723  distrlem5prl  7806  distrlem5pru  7807  ltexprlemell  7818  ltexprlemelu  7819  recexprlemm  7844  addsrmo  7963  mulsrmo  7964  addsrpr  7965  mulsrpr  7966  lttrsr  7982  recexgt0sr  7993  mulgt0sr  7998  ltresr  8059  axprecex  8100  axpre-lttrn  8104  axpre-mulgt0  8107  eqlelt  8266  lesub0  8659  apreap  8767  apreim  8783  aprcl  8826  aptap  8830  zltlen  9558  prime  9579  fzind  9595  qltlen  9874  xltnegi  10070  ixxval  10131  fzval  10245  fzdifsuc  10316  elfzm11  10326  elfzo  10384  zsupcllemex  10491  exbtwnzlemshrink  10509  rebtwn2zlemshrink  10514  facwordi  11003  zfz1iso  11106  pfxsuff1eqwrdeq  11284  wrd2ind  11308  shftfvalg  11396  shftfibg  11398  shftfval  11399  shftfib  11401  shftfn  11402  2shfti  11409  cau3lem  11692  caubnd2  11695  xrmaxiflemcom  11827  clim  11859  clim2  11861  climi  11865  climcn2  11887  addcn2  11888  subcn2  11889  mulcn2  11890  summodclem2a  11960  summodc  11962  fsum3  11966  fsumsplitf  11987  prodfdivap  12126  ntrivcvgap0  12128  prodeq1f  12131  prodeq2w  12135  prodeq2  12136  prodmodc  12157  zproddc  12158  fprodseq  12162  fprodntrivap  12163  fproddivapf  12210  fprodsplitf  12211  fprodsplit1f  12213  sinbnd  12331  cosbnd  12332  divalgb  12504  ndvdssub  12509  gcdval  12548  gcdneg  12571  bezoutlemstep  12586  bezoutlemmain  12587  bezoutlemex  12590  dfgcd2  12603  gcdass  12604  algcvgblem  12639  lcmval  12653  lcmneg  12664  lcmgcdlem  12667  lcmass  12675  qredeq  12686  prmind2  12710  euclemma  12736  pw2dvdslemn  12755  qnumval  12775  qdenval  12776  pceu  12886  pczpre  12888  pcdiv  12893  prmpwdvds  12946  prdsex  13370  gsumpropd  13493  gsumpropd2  13494  gsumress  13496  gsum0g  13497  mnd1  13556  grp1  13707  qusgrp2  13718  nmznsg  13818  releqgg  13825  eqgex  13826  iscmnd  13903  issrg  13997  iscrng2  14047  qusring2  14098  opprunitd  14143  crngunit  14144  dfrhm2  14187  rhmopp  14209  issubrng  14232  resrhm2b  14282  islmod  14324  lsssetm  14389  lsspropdg  14464  ixpsnbasval  14499  basis2  14791  eltg2  14796  isnei  14887  isneip  14889  restbasg  14911  iscnp  14942  iscnp3  14946  tgcn  14951  icnpimaex  14954  lmbrf  14958  cncnp  14973  cnptoprest2  14983  txbas  15001  txcnp  15014  imasnopn  15042  ispsmet  15066  ismet  15087  isxmet  15088  ismet2  15097  blres  15177  metcnp3  15254  txmetcnp  15261  mulcncf  15351  ellimc3apf  15403  limcdifap  15405  limcmpted  15406  limccnp2lem  15419  dvmptfsum  15468  elply2  15478  sincosq3sgn  15571  lgsquadlem1  15825  2sqlem8  15871  2sqlem9  15872  eupthres  16327  eupth2lem3lem6fi  16341  subctctexmid  16652  nnnninfex  16675  gfsumval  16732