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	|- (ph -> (ps <-> ch))

Assertion

Ref	Expression
anbi2d	|- (ph -> ((th /\ ps) <-> (th /\ ch)))

Proof of Theorem anbi2d

Step	Hyp	Ref	Expression
1		bid.1	. . 3 |- (ph -> (ps <-> ch))
2	1	a1d 22	. 2 |- (ph -> (th -> (ps <-> ch)))
3	2	pm5.32d 620	1 |- (ph -> ((th /\ ps) <-> (th /\ ch)))

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  2896  ceqsex6v  2900  vtocl2gaf  2922  ceqsrex2v  2975  moeq3  3014  mob2  3017  eqreu  3029  undif4  3608  r19.27z  3649  r19.27zv  3650  ssunsn2  3866  ralunsn  3880  intab  3957  preq12bg  4129  pw1in  4165  cnvkeq  4216  ins2keq  4219  ins3keq  4220  sikeq  4242  opkelopkabg  4246  opkelxpkg  4248  otkelins2kg  4254  otkelins3kg  4255  opkelcokg  4262  eladdc  4399  addcass  4416  nnsucelr  4429  nndisjeq  4430  opkltfing  4450  preaddccan2lem1  4455  lenltfin  4470  ncfineq  4474  ncfinraise  4482  ncfinlower  4484  tfineq  4489  evenodddisj  4517  nnpweq  4524  sfineq2  4528  sfindbl  4531  vfinspsslem1  4551  vfinspss  4552  phialllem1  4617  opabbid  4625  setconslem1  4732  xpeq2  4800  rabxp  4815  vtoclr  4817  opeliunxp  4821  opbrop  4842  brswap2  4861  brco  4884  dfres2  5003  xp11  5057  elxp4  5109  nfunv  5139  fununi  5161  fneq2  5175  fnun  5190  iunfopab  5205  feq3  5213  foeq3  5268  dffn5  5364  fvopab4t  5386  fvopab3g  5387  fvopab3ig  5388  isoeq2  5484  isoeq3  5485  f1oiso  5500  f1oiso2  5501  brswap  5510  oprabbid  5564  cbvoprab3  5572  fnov  5592  ov  5596  ov3  5600  ov6g  5601  ovg  5602  mpt2mptx  5709  brsnsi1  5776  trtxp  5782  brimage  5794  qrpprod  5837  dmpprod  5841  clos1eq2  5876  clos1conn  5880  trd  5922  brltc  6115  lecex  6116  tceq  6159  ceexlem1  6174  ce2le  6234  tcfnex  6245  nmembers1  6272  nchoicelem11  6300  nchoicelem16  6305  nchoicelem19  6308  fnfreclem3  6320