Theorem anbi2d 459

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 445	1 ⊢ (𝜑 → ((𝜃 ∧ 𝜓) ↔ (𝜃 ∧ 𝜒)))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  anbi2  462  anbi12d  464  bi2anan9  595  dn1dc  944  xorbi2d  1358  dfbi3dc  1375  xordidc  1377  eleq2w  2201  eleq2  2203  ceqsex2  2726  ceqsex6v  2730  vtocl2gaf  2753  ceqsrex2v  2817  mob2  2864  eqreu  2876  nelrdva  2891  dfss4st  3309  undif4  3425  r19.27m  3458  ifbi  3492  preq12bg  3700  opeq2  3706  ralunsn  3724  intab  3800  disjiun  3924  brimralrspcev  3987  opabbid  3993  opthg  4160  pocl  4225  ordelord  4303  ordtriexmid  4437  ontr2exmid  4440  onsucsssucexmid  4442  tfisi  4501  xpeq2  4554  rabxp  4576  vtoclr  4587  opeliunxp  4594  posng  4611  opbrop  4618  rexiunxp  4681  elrnmpt1  4790  dfres2  4871  brcodir  4926  poltletr  4939  xp11m  4977  elxp4  5026  elxp5  5027  dffun4f  5139  fununi  5191  fneq2  5212  fnun  5229  feq3  5257  foeq3  5343  funfveu  5434  funbrfv  5460  ssimaexg  5483  fvopab3g  5494  fvopab3ig  5495  fvelrn  5551  fmptco  5586  fsn2  5594  elunirn  5667  isoeq2  5703  isoeq3  5704  isocnv2  5713  isoini  5719  isopolem  5723  f1oiso  5727  f1oiso2  5728  oprabbid  5824  cbvoprab3  5847  mpomptx  5862  mpofun  5873  ov  5890  ovi3  5907  ov6g  5908  ovg  5909  caoftrn  6007  f1o2ndf1  6125  xporderlem  6128  f1od2  6132  brtpos2  6148  brtposg  6151  dftpos4  6160  recseq  6203  tfrlem3-2d  6209  tfrlemi1  6229  tfrexlem  6231  tfr1onlemaccex  6245  tfrcllemaccex  6258  tfrcl  6261  freceq1  6289  freceq2  6290  frecsuc  6304  nnaordex  6423  brecop  6519  eroveu  6520  erovlem  6521  ecopovtrn  6526  ecopovtrng  6529  th3qlem1  6531  th3qlem2  6532  th3q  6534  elpmg  6558  ixpsnval  6595  ixpsnf1o  6630  domeng  6646  dom2lem  6666  xpcomco  6720  xpassen  6724  xpdom2  6725  xpf1o  6738  phplem3g  6750  ssfiexmid  6770  domfiexmid  6772  findcard2  6783  findcard2s  6784  findcard2d  6785  findcard2sd  6786  diffifi  6788  fiintim  6817  fidcenumlemrk  6842  fidcenumlemr  6843  supeq2  6876  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  acfun  7063  ccfunen  7079  recexnq  7198  recmulnqg  7199  ltsonq  7206  enq0sym  7240  enq0ref  7241  enq0tr  7242  enq0breq  7244  addnq0mo  7255  mulnq0mo  7256  addnnnq0  7257  mulnnnq0  7258  elinp  7282  prdisj  7300  prarloclem3  7305  prarloc  7311  distrlem5prl  7394  distrlem5pru  7395  ltexprlemell  7406  ltexprlemelu  7407  recexprlemm  7432  addsrmo  7551  mulsrmo  7552  addsrpr  7553  mulsrpr  7554  lttrsr  7570  recexgt0sr  7581  mulgt0sr  7586  ltresr  7647  axprecex  7688  axpre-lttrn  7692  axpre-mulgt0  7695  lesub0  8241  apreap  8349  apreim  8365  aprcl  8408  zltlen  9129  prime  9150  fzind  9166  qltlen  9432  xltnegi  9618  ixxval  9679  fzval  9792  fzdifsuc  9861  elfzm11  9871  elfzo  9926  exbtwnzlemshrink  10026  rebtwn2zlemshrink  10031  facwordi  10486  zfz1iso  10584  shftfvalg  10590  shftfibg  10592  shftfval  10593  shftfib  10595  shftfn  10596  2shfti  10603  cau3lem  10886  caubnd2  10889  xrmaxiflemcom  11018  clim  11050  clim2  11052  climi  11056  climcn2  11078  addcn2  11079  subcn2  11080  mulcn2  11081  summodclem2a  11150  summodc  11152  fsum3  11156  fsumsplitf  11177  prodfdivap  11316  ntrivcvgap0  11318  prodeq1f  11321  prodeq2w  11325  prodeq2  11326  prodmodc  11347  sinbnd  11459  cosbnd  11460  divalgb  11622  ndvdssub  11627  zsupcllemex  11639  gcdval  11648  gcdneg  11670  bezoutlemstep  11685  bezoutlemmain  11686  bezoutlemex  11689  dfgcd2  11702  gcdass  11703  algcvgblem  11730  lcmval  11744  lcmneg  11755  lcmgcdlem  11758  lcmass  11766  qredeq  11777  prmind2  11801  euclemma  11824  pw2dvdslemn  11843  qnumval  11863  qdenval  11864  basis2  12215  eltg2  12222  isnei  12313  isneip  12315  restbasg  12337  iscnp  12368  iscnp3  12372  tgcn  12377  icnpimaex  12380  lmbrf  12384  cncnp  12399  cnptoprest2  12409  txbas  12427  txcnp  12440  imasnopn  12468  ispsmet  12492  ismet  12513  isxmet  12514  ismet2  12523  blres  12603  metcnp3  12680  txmetcnp  12687  mulcncf  12760  ellimc3apf  12798  limcdifap  12800  limcmpted  12801  limccnp2lem  12814  sincosq3sgn  12909  subctctexmid  13196