Theorem anbi2d 437

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 423	1 ⊢ (φ → ((θ ∧ ψ) ↔ (θ ∧ χ)))

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  anbi2  440  anbi12d  442  bi2anan9  538  dn1dc  866  xorbi2d  1269  dfbi3dc  1285  xordidc  1287  eleq2  2098  ceqsex2  2588  ceqsex6v  2592  vtocl2gaf  2614  ceqsrex2v  2670  mob2  2715  eqreu  2727  nelrdva  2740  psssstr  3045  undif4  3278  r19.27m  3310  ifbi  3342  preq12bg  3535  opeq2  3541  ralunsn  3559  intab  3635  opabbid  3813  opthg  3966  pocl  4031  ordelord  4084  ordtriexmid  4210  onsucsssucexmid  4212  tfisi  4253  xpeq2  4303  rabxp  4323  vtoclr  4331  opeliunxp  4338  posng  4355  opbrop  4362  rexiunxp  4421  elrnmpt1  4528  dfres2  4601  brcodir  4655  poltletr  4668  xp11m  4702  elxp4  4751  elxp5  4752  dffun4f  4861  fununi  4910  fneq2  4931  fnun  4948  feq3  4975  foeq3  5047  funfveu  5131  funbrfv  5155  ssimaexg  5178  fvopab3g  5188  fvopab3ig  5189  fvelrn  5241  fmptco  5273  fsn2  5280  elunirn  5348  isoeq2  5385  isoeq3  5386  isocnv2  5395  isoini  5400  isopolem  5404  f1oiso  5408  f1oiso2  5409  oprabbid  5500  cbvoprab3  5522  mpt2mptx  5537  mpt2fun  5545  ov  5562  ovi3  5579  ov6g  5580  ovg  5581  caoftrn  5678  f1o2ndf1  5791  xporderlem  5793  brtpos2  5807  brtposg  5810  dftpos4  5819  recseq  5862  tfrlem3-2  5868  tfrlem3-2d  5869  tfrlemi1  5887  tfrexlem  5889  freceq1  5919  freceq2  5920  frecsuc  5930  nnaordex  6036  brecop  6132  eroveu  6133  erovlem  6134  ecopovtrn  6139  ecopovtrng  6142  th3qlem1  6144  th3qlem2  6145  th3q  6147  domeng  6169  dom2lem  6188  xpcomco  6236  xpassen  6240  xpdom2  6241  ssfiexmid  6254  recexnq  6374  recmulnqg  6375  ltsonq  6382  enq0sym  6415  enq0ref  6416  enq0tr  6417  enq0breq  6419  addnq0mo  6430  mulnq0mo  6431  addnnnq0  6432  mulnnnq0  6433  elinp  6457  prdisj  6475  prarloclem3  6480  prarloc  6486  distrlem5prl  6562  distrlem5pru  6563  ltexprlemell  6572  ltexprlemelu  6573  recexprlemm  6596  addsrmo  6671  mulsrmo  6672  addsrpr  6673  mulsrpr  6674  lttrsr  6690  recexgt0sr  6701  mulgt0sr  6704  ltresr  6736  axprecex  6764  axpre-lttrn  6768  axpre-mulgt0  6771  lesub0  7269  apreap  7371  apreim  7387  zltlen  8095  prime  8113  fzind  8129  xltnegi  8518  ixxval  8535  fzval  8646  fzdifsuc  8713  elfzm11  8723  elfzo  8776