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  6414  enq0ref  6415  enq0tr  6416  enq0breq  6418  addnq0mo  6429  mulnq0mo  6430  addnnnq0  6431  mulnnnq0  6432  elinp  6456  prdisj  6474  prarloclem3  6479  prarloc  6485  distrlem5prl  6560  distrlem5pru  6561  ltexprlemell  6570  ltexprlemelu  6571  recexprlemm  6594  addsrmo  6631  mulsrmo  6632  addsrpr  6633  mulsrpr  6634  lttrsr  6650  recexgt0sr  6661  mulgt0sr  6664  ltresr  6696  axprecex  6724  axpre-lttrn  6728  axpre-mulgt0  6731  lesub0  7229  apreap  7331  apreim  7347  zltlen  8055  prime  8073  fzind  8089  xltnegi  8478  ixxval  8495  fzval  8606  fzdifsuc  8673  elfzm11  8683  elfzo  8736