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  523  dn1dc  849  xorbi2d  1250  dfbi3dc  1266  xordidc  1268  eleq2  2074  ceqsex2  2562  ceqsex6v  2566  vtocl2gaf  2588  ceqsrex2v  2644  mob2  2689  eqreu  2701  nelrdva  2714  psssstr  3019  undif4  3252  r19.27m  3284  ifbi  3314  preq12bg  3507  opeq2  3513  ralunsn  3531  intab  3607  opabbid  3785  opthg  3938  pocl  4003  ordelord  4056  ordtriexmid  4182  onsucsssucexmid  4184  tfisi  4225  xpeq2  4275  rabxp  4295  vtoclr  4303  opeliunxp  4310  posng  4327  opbrop  4334  rexiunxp  4393  elrnmpt1  4500  dfres2  4573  brcodir  4627  poltletr  4640  xp11m  4674  elxp4  4723  elxp5  4724  dffun4f  4832  fununi  4881  fneq2  4902  fnun  4919  feq3  4946  foeq3  5017  funfveu  5101  funbrfv  5125  ssimaexg  5148  fvopab3g  5158  fvopab3ig  5159  fvelrn  5211  fmptco  5243  fsn2  5250  elunirn  5318  isoeq2  5355  isoeq3  5356  isocnv2  5365  isoini  5370  isopolem  5374  f1oiso  5378  f1oiso2  5379  oprabbid  5469  cbvoprab3  5491  mpt2mptx  5506  mpt2fun  5514  ov  5531  ovi3  5548  ov6g  5549  ovg  5550  caoftrn  5647  f1o2ndf1  5760  xporderlem  5762  brtpos2  5776  brtposg  5779  dftpos4  5788  recseq  5831  tfrlem3-2  5837  tfrlem3-2d  5838  tfrlemi1  5855  tfrexlem  5858  frecsuc  5895  nnaordex  5999  brecop  6095  eroveu  6096  erovlem  6097  ecopovtrn  6102  ecopovtrng  6105  th3qlem1  6107  th3qlem2  6108  th3q  6110  recexnq  6235  recmulnqg  6236  ltsonq  6243  enq0sym  6273  enq0ref  6274  enq0tr  6275  enq0breq  6277  addnq0mo  6288  mulnq0mo  6289  addnnnq0  6290  mulnnnq0  6291  elinp  6314  prdisj  6332  prarloclem3  6337  prarloc  6343  distrlem5prl  6411  distrlem5pru  6412  ltexprlemell  6421  ltexprlemelu  6422  recexprlemm  6445  addsrmo  6481  mulsrmo  6482  addsrpr  6483  mulsrpr  6484  lttrsr  6500  recexgt0sr  6511  mulgt0sr  6514  ltresr  6545  axprecex  6569  axpre-lttrn  6573  axpre-mulgt0  6576  lesub0  7072  apreap  7174  apreim  7190  zltlen  7884  prime  7901  fzind  7917