Theorem anbi2d 451

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

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  anbi2  454  anbi12d  456  bi2anan9  570  dn1dc  901  xorbi2d  1311  dfbi3dc  1328  xordidc  1330  eleq2  2142  ceqsex2  2639  ceqsex6v  2643  vtocl2gaf  2665  ceqsrex2v  2727  mob2  2772  eqreu  2784  nelrdva  2797  undif4  3306  r19.27m  3336  ifbi  3369  preq12bg  3565  opeq2  3571  ralunsn  3589  intab  3665  opabbid  3843  opthg  3993  pocl  4058  ordelord  4136  ordtriexmid  4265  ontr2exmid  4268  onsucsssucexmid  4270  tfisi  4328  xpeq2  4378  rabxp  4398  vtoclr  4406  opeliunxp  4413  posng  4430  opbrop  4437  rexiunxp  4496  elrnmpt1  4603  dfres2  4678  brcodir  4732  poltletr  4745  xp11m  4779  elxp4  4828  elxp5  4829  dffun4f  4938  fununi  4987  fneq2  5008  fnun  5025  feq3  5052  foeq3  5124  funfveu  5208  funbrfv  5233  ssimaexg  5256  fvopab3g  5266  fvopab3ig  5267  fvelrn  5319  fmptco  5351  fsn2  5358  elunirn  5426  isoeq2  5462  isoeq3  5463  isocnv2  5472  isoini  5477  isopolem  5481  f1oiso  5485  f1oiso2  5486  oprabbid  5578  cbvoprab3  5600  mpt2mptx  5615  mpt2fun  5623  ov  5640  ovi3  5657  ov6g  5658  ovg  5659  caoftrn  5756  f1o2ndf1  5869  xporderlem  5872  f1od2  5876  brtpos2  5889  brtposg  5892  dftpos4  5901  recseq  5944  tfrlem3-2  5950  tfrlem3-2d  5951  tfrlemi1  5969  tfrexlem  5971  freceq1  6002  freceq2  6003  frecsuc  6014  nnaordex  6123  brecop  6219  eroveu  6220  erovlem  6221  ecopovtrn  6226  ecopovtrng  6229  th3qlem1  6231  th3qlem2  6232  th3q  6234  domeng  6256  dom2lem  6275  xpcomco  6323  xpassen  6327  xpdom2  6328  phplem3g  6342  ssfiexmid  6361  domfiexmid  6363  findcard2  6373  findcard2s  6374  findcard2d  6375  findcard2sd  6376  diffifi  6378  supeq2  6402  recexnq  6580  recmulnqg  6581  ltsonq  6588  enq0sym  6622  enq0ref  6623  enq0tr  6624  enq0breq  6626  addnq0mo  6637  mulnq0mo  6638  addnnnq0  6639  mulnnnq0  6640  elinp  6664  prdisj  6682  prarloclem3  6687  prarloc  6693  distrlem5prl  6776  distrlem5pru  6777  ltexprlemell  6788  ltexprlemelu  6789  recexprlemm  6814  addsrmo  6920  mulsrmo  6921  addsrpr  6922  mulsrpr  6923  lttrsr  6939  recexgt0sr  6950  mulgt0sr  6954  ltresr  7007  axprecex  7046  axpre-lttrn  7050  axpre-mulgt0  7053  lesub0  7583  apreap  7687  apreim  7703  zltlen  8426  prime  8446  fzind  8462  qltlen  8725  xltnegi  8902  ixxval  8919  fzval  9031  fzdifsuc  9098  elfzm11  9108  elfzo  9159  qbtwnzlemshrink  9258  rebtwn2zlemshrink  9262  facwordi  9667  shftfvalg  9706  shftfibg  9708  shftfval  9709  shftfib  9711  shftfn  9712  2shfti  9719  cau3lem  10000  caubnd2  10003  clim  10120  clim2  10122  climi  10126  climcn2  10148  addcn2  10149  subcn2  10150  mulcn2  10151  divalgb  10325  ndvdssub  10330  zsupcllemex  10342  gcdval  10351  gcdneg  10373  bezoutlemstep  10386  bezoutlemmain  10387  bezoutlemex  10390  dfgcd2  10403  gcdass  10404  algcvgblem  10431  lcmval  10445  lcmneg  10456  lcmgcdlem  10459  lcmass  10467  qredeq  10478  prmind2  10502  euclemma  10525  pw2dvdslemn  10543