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  6526  brtposg  6529  dftpos4  6538  recseq  6581  tfrlem3-2d  6587  tfrlemi1  6607  tfrexlem  6609  tfr1onlemaccex  6623  tfrcllemaccex  6636  tfrcl  6639  freceq1  6667  freceq2  6668  frecsuc  6682  nnaordex  6805  brecop  6903  eroveu  6904  erovlem  6905  ecopovtrn  6910  ecopovtrng  6913  th3qlem1  6915  th3qlem2  6916  th3q  6918  elpmg  6942  ixpsnval  6987  ixpsnf1o  7022  domeng  7040  dom2lem  7062  mapsnend  7103  modom  7112  xpcomco  7128  xpassen  7132  xpdom2  7133  xpf1o  7148  phplem3g  7161  ssfiexmid  7182  ssfiexmidt  7184  domfiexmid  7186  findcard2  7197  findcard2s  7198  findcard2d  7199  findcard2sd  7200  diffifi  7202  fiintim  7242  opabfi  7251  fidcenumlemrk  7276  fidcenumlemr  7277  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  9735  prime  9756  fzind  9772  qltlen  10056  xltnegi  10254  ixxval  10315  fzval  10430  fzdifsuc  10505  elfzm11  10515  elfzo  10573  zsupcllemex  10680  exbtwnzlemshrink  10700  rebtwn2zlemshrink  10705  facwordi  11200  zfz1iso  11315  pfxsuff1eqwrdeq  11493  wrd2ind  11517  shftfvalg  11605  shftfibg  11607  shftfval  11608  shftfib  11610  shftfn  11611  2shfti  11618  cau3lem  11903  caubnd2  11906  xrmaxiflemcom  12040  clim  12072  clim2  12074  climi  12078  climcn2  12100  addcn2  12101  subcn2  12102  mulcn2  12103  summodclem2a  12173  summodc  12175  fsum3  12179  fsumsplitf  12200  prodfdivap  12339  ntrivcvgap0  12341  prodeq1f  12344  prodeq2w  12348  prodeq2  12349  prodmodc  12370  zproddc  12371  fprodseq  12375  fprodntrivap  12376  fproddivapf  12423  fprodsplitf  12424  fprodsplit1f  12426  sinbnd  12544  cosbnd  12545  divalgb  12717  ndvdssub  12722  gcdval  12761  gcdneg  12784  bezoutlemstep  12799  bezoutlemmain  12800  bezoutlemex  12803  dfgcd2  12816  gcdass  12817  algcvgblem  12852  lcmval  12866  lcmneg  12877  lcmgcdlem  12880  lcmass  12888  qredeq  12899  prmind2  12923  euclemma  12950  pwbdvdslemn  12969  qnumval  12990  qdenval  12991  pceu  13103  pczpre  13105  pcdiv  13110  prmpwdvds  13163  gzsumress  13771  gzsum0  13772  mnd1  13821  grp1  13970  qusgrp2  13975  nmznsg  14075  releqgg  14082  eqgex  14083  resscntz  14166  iscmnd  14191  gsumvalfi  14242  prdsex  14279  issrg  14376  iscrng2  14426  qusring2  14480  opprunitd  14526  crngunit  14527  dfrhm2  14570  rhmopp  14592  issubrng  14616  resrhm2b  14666  islmod  14736  lsssetm  14802  lsspropdg  14877  ixpsnbasval  14912  basis2  15274  eltg2  15279  isnei  15370  isneip  15372  restbasg  15394  iscnp  15425  iscnp3  15429  tgcn  15434  icnpimaex  15437  lmbrf  15441  cncnp  15456  cnptoprest2  15466  txbas  15484  txcnp  15497  imasnopn  15525  ispsmet  15549  ismet  15570  isxmet  15571  ismet2  15580  blres  15660  metcnp3  15737  txmetcnp  15744  mulcncf  15834  ellimc3apf  15886  limcdifap  15888  limcmpted  15889  limccnp2lem  15902  dvmptfsum  15951  elply2  15961  sincosq3sgn  16055  zprmlogbaplem3  16217  pellexlem3  16231  lgsquadlem1  16401  2sqlem8  16447  2sqlem9  16448  eupthres  16903  eupth2lem3lem6fi  16917  subctctexmid  17235  wexmiddifxy  17251  nnnninfex  17271