Theorem anbi2d 684

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
bid.1	⊢ (φ → (ψ ↔ χ))

Assertion

Ref	Expression
anbi2d	⊢ (φ → ((θ ∧ ψ) ↔ (θ ∧ χ)))

Proof of Theorem anbi2d

Step	Hyp	Ref	Expression
1		bid.1	. . 3 ⊢ (φ → (ψ ↔ χ))
2	1	a1d 22	. 2 ⊢ (φ → (θ → (ψ ↔ χ)))
3	2	pm5.32d 620	1 ⊢ (φ → ((θ ∧ ψ) ↔ (θ ∧ χ)))

Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  anbi2  688  anbi12d  691  bi2anan9  843  2eu6  2289  eleq2  2414  ceqsex2  2895  ceqsex6v  2899  vtocl2gaf  2921  ceqsrex2v  2974  moeq3  3013  mob2  3016  eqreu  3028  undif4  3607  r19.27z  3648  r19.27zv  3649  ssunsn2  3865  ralunsn  3879  intab  3956  preq12bg  4128  pw1in  4164  cnvkeq  4215  ins2keq  4218  ins3keq  4219  sikeq  4241  opkelopkabg  4245  opkelxpkg  4247  otkelins2kg  4253  otkelins3kg  4254  opkelcokg  4261  eladdc  4398  addcass  4415  nnsucelr  4428  nndisjeq  4429  opkltfing  4449  preaddccan2lem1  4454  lenltfin  4469  ncfineq  4473  ncfinraise  4481  ncfinlower  4483  tfineq  4488  evenodddisj  4516  nnpweq  4523  sfineq2  4527  sfindbl  4530  vfinspsslem1  4550  vfinspss  4551  phialllem1  4616  opabbid  4624  setconslem1  4731  xpeq2  4799  rabxp  4814  vtoclr  4816  opeliunxp  4820  opbrop  4841  brswap2  4860  brco  4883  dfres2  5002  xp11  5056  elxp4  5108  nfunv  5138  fununi  5160  fneq2  5174  fnun  5189  iunfopab  5204  feq3  5212  foeq3  5267  dffn5  5363  fvopab4t  5385  fvopab3g  5386  fvopab3ig  5387  isoeq2  5483  isoeq3  5484  f1oiso  5499  f1oiso2  5500  brswap  5509  oprabbid  5563  cbvoprab3  5571  fnov  5591  ov  5595  ov3  5599  ov6g  5600  ovg  5601  mpt2mptx  5708  brsnsi1  5775  trtxp  5781  brimage  5793  qrpprod  5836  dmpprod  5840  clos1eq2  5875  clos1conn  5879  trd  5921  brltc  6114  lecex  6115  tceq  6158  ceexlem1  6173  ce2le  6233  tcfnex  6244  nmembers1  6271  nchoicelem11  6299  nchoicelem16  6304  nchoicelem19  6307  fnfreclem3  6319