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  2777  ceqsex6v  2781  vtocl2gaf  2804  ceqsrex2v  2869  mob2  2917  eqreu  2929  nelrdva  2944  dfss4st  3368  undif4  3485  r19.27m  3518  ifbi  3554  preq12bg  3772  opeq2  3778  ralunsn  3796  intab  3872  disjiun  3996  brimralrspcev  4060  opabbid  4066  opthg  4236  pocl  4301  ordelord  4379  ordtriexmid  4518  ontr2exmid  4522  onsucsssucexmid  4524  tfisi  4584  xpeq2  4639  rabxp  4661  vtoclr  4672  opeliunxp  4679  posng  4696  opbrop  4703  rexiunxp  4766  elrnmpt1  4875  dfres2  4956  brcodir  5013  poltletr  5026  xp11m  5064  elxp4  5113  elxp5  5114  dffun4f  5229  fununi  5281  fneq2  5302  fnun  5319  feq3  5347  foeq3  5433  funfveu  5525  funbrfv  5551  ssimaexg  5575  fvopab3g  5586  fvopab3ig  5587  fvelrn  5644  fmptco  5679  fsn2  5687  elunirn  5762  isoeq2  5798  isoeq3  5799  isocnv2  5808  isoini  5814  isopolem  5818  f1oiso  5822  f1oiso2  5823  oprabbid  5923  cbvoprab3  5946  mpomptx  5961  mpofun  5972  ov  5989  ovi3  6006  ov6g  6007  ovg  6008  caoftrn  6103  f1o2ndf1  6224  xporderlem  6227  f1od2  6231  brtpos2  6247  brtposg  6250  dftpos4  6259  recseq  6302  tfrlem3-2d  6308  tfrlemi1  6328  tfrexlem  6330  tfr1onlemaccex  6344  tfrcllemaccex  6357  tfrcl  6360  freceq1  6388  freceq2  6389  frecsuc  6403  nnaordex  6524  brecop  6620  eroveu  6621  erovlem  6622  ecopovtrn  6627  ecopovtrng  6630  th3qlem1  6632  th3qlem2  6633  th3q  6635  elpmg  6659  ixpsnval  6696  ixpsnf1o  6731  domeng  6747  dom2lem  6767  xpcomco  6821  xpassen  6825  xpdom2  6826  xpf1o  6839  phplem3g  6851  ssfiexmid  6871  domfiexmid  6873  findcard2  6884  findcard2s  6885  findcard2d  6886  findcard2sd  6887  diffifi  6889  fiintim  6923  fidcenumlemrk  6948  fidcenumlemr  6949  supeq2  6983  nnnninfeq2  7122  exmidfodomrlemr  7196  exmidfodomrlemrALT  7197  acfun  7201  2omotaplemap  7251  2omotaplemst  7252  exmidapne  7254  ccfunen  7258  recexnq  7384  recmulnqg  7385  ltsonq  7392  enq0sym  7426  enq0ref  7427  enq0tr  7428  enq0breq  7430  addnq0mo  7441  mulnq0mo  7442  addnnnq0  7443  mulnnnq0  7444  elinp  7468  prdisj  7486  prarloclem3  7491  prarloc  7497  distrlem5prl  7580  distrlem5pru  7581  ltexprlemell  7592  ltexprlemelu  7593  recexprlemm  7618  addsrmo  7737  mulsrmo  7738  addsrpr  7739  mulsrpr  7740  lttrsr  7756  recexgt0sr  7767  mulgt0sr  7772  ltresr  7833  axprecex  7874  axpre-lttrn  7878  axpre-mulgt0  7881  eqlelt  8038  lesub0  8430  apreap  8538  apreim  8554  aprcl  8597  aptap  8601  zltlen  9325  prime  9346  fzind  9362  qltlen  9634  xltnegi  9829  ixxval  9890  fzval  10004  fzdifsuc  10074  elfzm11  10084  elfzo  10142  exbtwnzlemshrink  10242  rebtwn2zlemshrink  10247  facwordi  10711  zfz1iso  10812  shftfvalg  10818  shftfibg  10820  shftfval  10821  shftfib  10823  shftfn  10824  2shfti  10831  cau3lem  11114  caubnd2  11117  xrmaxiflemcom  11248  clim  11280  clim2  11282  climi  11286  climcn2  11308  addcn2  11309  subcn2  11310  mulcn2  11311  summodclem2a  11380  summodc  11382  fsum3  11386  fsumsplitf  11407  prodfdivap  11546  ntrivcvgap0  11548  prodeq1f  11551  prodeq2w  11555  prodeq2  11556  prodmodc  11577  zproddc  11578  fprodseq  11582  fprodntrivap  11583  fproddivapf  11630  fprodsplitf  11631  fprodsplit1f  11633  sinbnd  11751  cosbnd  11752  divalgb  11920  ndvdssub  11925  zsupcllemex  11937  gcdval  11950  gcdneg  11973  bezoutlemstep  11988  bezoutlemmain  11989  bezoutlemex  11992  dfgcd2  12005  gcdass  12006  algcvgblem  12039  lcmval  12053  lcmneg  12064  lcmgcdlem  12067  lcmass  12075  qredeq  12086  prmind2  12110  euclemma  12136  pw2dvdslemn  12155  qnumval  12175  qdenval  12176  pceu  12285  pczpre  12287  pcdiv  12292  prmpwdvds  12343  mnd1  12775  grp1  12904  iscmnd  13001  issrg  13048  iscrng2  13098  opprunitd  13178  crngunit  13179  basis2  13328  eltg2  13335  isnei  13426  isneip  13428  restbasg  13450  iscnp  13481  iscnp3  13485  tgcn  13490  icnpimaex  13493  lmbrf  13497  cncnp  13512  cnptoprest2  13522  txbas  13540  txcnp  13553  imasnopn  13581  ispsmet  13605  ismet  13626  isxmet  13627  ismet2  13636  blres  13716  metcnp3  13793  txmetcnp  13800  mulcncf  13873  ellimc3apf  13911  limcdifap  13913  limcmpted  13914  limccnp2lem  13927  sincosq3sgn  14031  2sqlem8  14241  2sqlem9  14242  subctctexmid  14521