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  969  dfifp3dc  991  ifpdfbidc  994  xorbi2d  1425  dfbi3dc  1442  xordidc  1444  eleq2w  2296  eleq2  2298  ceqsex2  2857  ceqsex6v  2861  vtocl2gaf  2884  ceqsrex2v  2952  mob2  3000  eqreu  3012  nelrdva  3027  dfss4st  3458  undif4  3575  r19.27m  3609  ifbi  3647  preq12bg  3882  opeq2  3889  ralunsn  3907  intab  3983  disjiun  4109  brimralrspcev  4174  opabbid  4180  opthg  4359  pocl  4429  ordelord  4507  ordtriexmid  4648  ontr2exmid  4652  onsucsssucexmid  4654  tfisi  4714  xpeq2  4769  rabxp  4792  vtoclr  4803  opeliunxp  4810  posng  4827  opbrop  4834  rexiunxp  4902  elrnmpt1  5013  dfres2  5095  brcodir  5155  poltletr  5168  xp11m  5206  elxp4  5255  elxp5  5256  dffun4f  5373  fununi  5429  fneq2  5450  fnun  5469  feq3  5498  foeq3  5593  funfveu  5688  funbrfv  5718  ssimaexg  5744  fvopab3g  5755  fvopab3ig  5756  fvelrn  5813  fmptco  5848  fsn2  5856  elunirn  5945  isoeq2  5981  isoeq3  5982  isocnv2  5991  isoini  5997  isopolem  6001  f1oiso  6005  f1oiso2  6006  oprabbid  6114  cbvoprab3  6137  mpomptx  6152  mpofun  6163  ov  6181  ovi3  6199  ov6g  6200  ovg  6201  caoftrn  6308  uchoice  6344  f1o2ndf1  6437  xporderlem  6440  f1od2  6444  suppimacnvfn  6459  brtpos2  6495  brtposg  6498  dftpos4  6507  recseq  6550  tfrlem3-2d  6556  tfrlemi1  6576  tfrexlem  6578  tfr1onlemaccex  6592  tfrcllemaccex  6605  tfrcl  6608  freceq1  6636  freceq2  6637  frecsuc  6651  nnaordex  6774  brecop  6872  eroveu  6873  erovlem  6874  ecopovtrn  6879  ecopovtrng  6882  th3qlem1  6884  th3qlem2  6885  th3q  6887  elpmg  6911  ixpsnval  6949  ixpsnf1o  6984  domeng  7002  dom2lem  7024  mapsnend  7065  modom  7074  xpcomco  7090  xpassen  7094  xpdom2  7095  xpf1o  7110  phplem3g  7123  ssfiexmid  7144  ssfiexmidt  7146  domfiexmid  7148  findcard2  7159  findcard2s  7160  findcard2d  7161  findcard2sd  7162  diffifi  7164  fiintim  7204  opabfi  7213  fidcenumlemrk  7237  fidcenumlemr  7238  supeq2  7293  nninfninc  7427  nnnninfeq2  7433  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  isacnm  7523  acfun  7527  2omotaplemap  7587  2omotaplemst  7588  exmidapne  7590  ccfunen  7594  recexnq  7721  recmulnqg  7722  ltsonq  7729  enq0sym  7763  enq0ref  7764  enq0tr  7765  enq0breq  7767  addnq0mo  7778  mulnq0mo  7779  addnnnq0  7780  mulnnnq0  7781  elinp  7805  prdisj  7823  prarloclem3  7828  prarloc  7834  distrlem5prl  7917  distrlem5pru  7918  ltexprlemell  7929  ltexprlemelu  7930  recexprlemm  7955  addsrmo  8074  mulsrmo  8075  addsrpr  8076  mulsrpr  8077  lttrsr  8093  recexgt0sr  8104  mulgt0sr  8109  ltresr  8170  axprecex  8211  axpre-lttrn  8215  axpre-mulgt0  8218  eqlelt  8376  lesub0  8770  apreap  8878  apreim  8894  aprcl  8937  aptap  8941  zltlen  9674  prime  9695  fzind  9711  qltlen  9990  xltnegi  10187  ixxval  10248  fzval  10363  fzdifsuc  10437  elfzm11  10447  elfzo  10505  zsupcllemex  10612  exbtwnzlemshrink  10632  rebtwn2zlemshrink  10637  facwordi  11127  zfz1iso  11238  pfxsuff1eqwrdeq  11416  wrd2ind  11440  shftfvalg  11528  shftfibg  11530  shftfval  11531  shftfib  11533  shftfn  11534  2shfti  11541  cau3lem  11824  caubnd2  11827  xrmaxiflemcom  11959  clim  11991  clim2  11993  climi  11997  climcn2  12019  addcn2  12020  subcn2  12021  mulcn2  12022  summodclem2a  12092  summodc  12094  fsum3  12098  fsumsplitf  12119  prodfdivap  12258  ntrivcvgap0  12260  prodeq1f  12263  prodeq2w  12267  prodeq2  12268  prodmodc  12289  zproddc  12290  fprodseq  12294  fprodntrivap  12295  fproddivapf  12342  fprodsplitf  12343  fprodsplit1f  12345  sinbnd  12463  cosbnd  12464  divalgb  12636  ndvdssub  12641  gcdval  12680  gcdneg  12703  bezoutlemstep  12718  bezoutlemmain  12719  bezoutlemex  12722  dfgcd2  12735  gcdass  12736  algcvgblem  12771  lcmval  12785  lcmneg  12796  lcmgcdlem  12799  lcmass  12807  qredeq  12818  prmind2  12842  euclemma  12868  pw2dvdslemn  12887  qnumval  12907  qdenval  12908  pceu  13018  pczpre  13020  pcdiv  13025  prmpwdvds  13078  gsumpropd  13655  gsumpropd2  13656  gsumress  13658  gsum0g  13659  mnd1  13710  grp1  13861  qusgrp2  13866  nmznsg  13966  releqgg  13973  eqgex  13974  iscmnd  14051  gfsumval  14102  prdsex  14114  issrg  14208  iscrng2  14258  qusring2  14309  opprunitd  14355  crngunit  14356  dfrhm2  14399  rhmopp  14421  issubrng  14445  resrhm2b  14495  islmod  14565  lsssetm  14630  lsspropdg  14705  ixpsnbasval  14740  basis2  15039  eltg2  15044  isnei  15135  isneip  15137  restbasg  15159  iscnp  15190  iscnp3  15194  tgcn  15199  icnpimaex  15202  lmbrf  15206  cncnp  15221  cnptoprest2  15231  txbas  15249  txcnp  15262  imasnopn  15290  ispsmet  15314  ismet  15335  isxmet  15336  ismet2  15345  blres  15425  metcnp3  15502  txmetcnp  15509  mulcncf  15599  ellimc3apf  15651  limcdifap  15653  limcmpted  15654  limccnp2lem  15667  dvmptfsum  15716  elply2  15726  sincosq3sgn  15819  pellexlem3  15973  lgsquadlem1  16076  2sqlem8  16122  2sqlem9  16123  eupthres  16578  eupth2lem3lem6fi  16592  subctctexmid  16900  nnnninfex  16926