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  606  dn1dc  960  xorbi2d  1380  dfbi3dc  1397  xordidc  1399  eleq2w  2239  eleq2  2241  ceqsex2  2778  ceqsex6v  2782  vtocl2gaf  2805  ceqsrex2v  2870  mob2  2918  eqreu  2930  nelrdva  2945  dfss4st  3369  undif4  3486  r19.27m  3519  ifbi  3555  preq12bg  3774  opeq2  3780  ralunsn  3798  intab  3874  disjiun  3999  brimralrspcev  4063  opabbid  4069  opthg  4239  pocl  4304  ordelord  4382  ordtriexmid  4521  ontr2exmid  4525  onsucsssucexmid  4527  tfisi  4587  xpeq2  4642  rabxp  4664  vtoclr  4675  opeliunxp  4682  posng  4699  opbrop  4706  rexiunxp  4770  elrnmpt1  4879  dfres2  4960  brcodir  5017  poltletr  5030  xp11m  5068  elxp4  5117  elxp5  5118  dffun4f  5233  fununi  5285  fneq2  5306  fnun  5323  feq3  5351  foeq3  5437  funfveu  5529  funbrfv  5555  ssimaexg  5579  fvopab3g  5590  fvopab3ig  5591  fvelrn  5648  fmptco  5683  fsn2  5691  elunirn  5767  isoeq2  5803  isoeq3  5804  isocnv2  5813  isoini  5819  isopolem  5823  f1oiso  5827  f1oiso2  5828  oprabbid  5928  cbvoprab3  5951  mpomptx  5966  mpofun  5977  ov  5994  ovi3  6011  ov6g  6012  ovg  6013  caoftrn  6108  f1o2ndf1  6229  xporderlem  6232  f1od2  6236  brtpos2  6252  brtposg  6255  dftpos4  6264  recseq  6307  tfrlem3-2d  6313  tfrlemi1  6333  tfrexlem  6335  tfr1onlemaccex  6349  tfrcllemaccex  6362  tfrcl  6365  freceq1  6393  freceq2  6394  frecsuc  6408  nnaordex  6529  brecop  6625  eroveu  6626  erovlem  6627  ecopovtrn  6632  ecopovtrng  6635  th3qlem1  6637  th3qlem2  6638  th3q  6640  elpmg  6664  ixpsnval  6701  ixpsnf1o  6736  domeng  6752  dom2lem  6772  xpcomco  6826  xpassen  6830  xpdom2  6831  xpf1o  6844  phplem3g  6856  ssfiexmid  6876  domfiexmid  6878  findcard2  6889  findcard2s  6890  findcard2d  6891  findcard2sd  6892  diffifi  6894  fiintim  6928  fidcenumlemrk  6953  fidcenumlemr  6954  supeq2  6988  nnnninfeq2  7127  exmidfodomrlemr  7201  exmidfodomrlemrALT  7202  acfun  7206  2omotaplemap  7256  2omotaplemst  7257  exmidapne  7259  ccfunen  7263  recexnq  7389  recmulnqg  7390  ltsonq  7397  enq0sym  7431  enq0ref  7432  enq0tr  7433  enq0breq  7435  addnq0mo  7446  mulnq0mo  7447  addnnnq0  7448  mulnnnq0  7449  elinp  7473  prdisj  7491  prarloclem3  7496  prarloc  7502  distrlem5prl  7585  distrlem5pru  7586  ltexprlemell  7597  ltexprlemelu  7598  recexprlemm  7623  addsrmo  7742  mulsrmo  7743  addsrpr  7744  mulsrpr  7745  lttrsr  7761  recexgt0sr  7772  mulgt0sr  7777  ltresr  7838  axprecex  7879  axpre-lttrn  7883  axpre-mulgt0  7886  eqlelt  8044  lesub0  8436  apreap  8544  apreim  8560  aprcl  8603  aptap  8607  zltlen  9331  prime  9352  fzind  9368  qltlen  9640  xltnegi  9835  ixxval  9896  fzval  10010  fzdifsuc  10081  elfzm11  10091  elfzo  10149  exbtwnzlemshrink  10249  rebtwn2zlemshrink  10254  facwordi  10720  zfz1iso  10821  shftfvalg  10827  shftfibg  10829  shftfval  10830  shftfib  10832  shftfn  10833  2shfti  10840  cau3lem  11123  caubnd2  11126  xrmaxiflemcom  11257  clim  11289  clim2  11291  climi  11295  climcn2  11317  addcn2  11318  subcn2  11319  mulcn2  11320  summodclem2a  11389  summodc  11391  fsum3  11395  fsumsplitf  11416  prodfdivap  11555  ntrivcvgap0  11557  prodeq1f  11560  prodeq2w  11564  prodeq2  11565  prodmodc  11586  zproddc  11587  fprodseq  11591  fprodntrivap  11592  fproddivapf  11639  fprodsplitf  11640  fprodsplit1f  11642  sinbnd  11760  cosbnd  11761  divalgb  11930  ndvdssub  11935  zsupcllemex  11947  gcdval  11960  gcdneg  11983  bezoutlemstep  11998  bezoutlemmain  11999  bezoutlemex  12002  dfgcd2  12015  gcdass  12016  algcvgblem  12049  lcmval  12063  lcmneg  12074  lcmgcdlem  12077  lcmass  12085  qredeq  12096  prmind2  12120  euclemma  12146  pw2dvdslemn  12165  qnumval  12185  qdenval  12186  pceu  12295  pczpre  12297  pcdiv  12302  prmpwdvds  12353  prdsex  12718  mnd1  12847  grp1  12976  nmznsg  13073  releqgg  13080  iscmnd  13101  issrg  13148  iscrng2  13198  opprunitd  13279  crngunit  13280  islmod  13381  basis2  13551  eltg2  13556  isnei  13647  isneip  13649  restbasg  13671  iscnp  13702  iscnp3  13706  tgcn  13711  icnpimaex  13714  lmbrf  13718  cncnp  13733  cnptoprest2  13743  txbas  13761  txcnp  13774  imasnopn  13802  ispsmet  13826  ismet  13847  isxmet  13848  ismet2  13857  blres  13937  metcnp3  14014  txmetcnp  14021  mulcncf  14094  ellimc3apf  14132  limcdifap  14134  limcmpted  14135  limccnp2lem  14148  sincosq3sgn  14252  2sqlem8  14473  2sqlem9  14474  subctctexmid  14753