Theorem anbi1d 685

Description: Deduction adding a right 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
anbi1d	|- (ph -> ((ps /\ th) <-> (ch /\ th)))

Proof of Theorem anbi1d

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

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:  anbi1  687  anbi12d  691  bi2anan9  843  pm5.71  902  cador  1391  drsb1  2022  eleq1  2413  rexeqf  2804  reueq1f  2805  rmoeq1f  2806  rabeqf  2852  vtocl2gaf  2921  alexeq  2968  ceqex  2969  sbc2or  3054  sbc5  3070  rexss  3333  psstr  3373  ineq1  3450  difin2  3516  r19.28z  3642  r19.28zv  3645  ssunsn2  3865  eluni  3894  pwadjoin  4119  preq12bg  4128  elxpk  4196  opkelopkabg  4245  opkelxpkg  4247  otkelins2kg  4253  otkelins3kg  4254  opkelcokg  4261  opkelimagekg  4271  insklem  4304  ssfin  4470  ncfinraise  4481  evenodddisj  4516  nnpweq  4523  sfineq1  4526  vfinspss  4551  copsexg  4607  elopab  4696  setconslem6  4736  xpeq1  4798  elxpi  4800  vtoclr  4816  opbrop  4841  brswap2  4860  brco  4883  resopab2  5001  elxp4  5108  fun11  5159  feq2  5211  f1eq2  5254  f1eq3  5255  foeq2  5266  tz6.12-2  5346  dmfco  5381  respreima  5410  isoeq5  5486  isomin  5496  isoini  5497  f1oiso  5499  f1oiso2  5500  brswap  5509  oprabid  5550  dfoprab2  5558  eloprabga  5578  resoprab  5581  resoprab2  5582  ov  5595  ov3  5599  ov6g  5600  ovg  5601  mpteq12f  5655  mpt2eq123  5661  trtxp  5781  oqelins4  5794  txpcofun  5803  qrpprod  5836  dmpprod  5840  clos1eq1  5874  trd  5921  frd  5922  elpmg  6013  lecex  6115  ncspw1eu  6159  leltctr  6212  ce2le  6233  nmembers1lem1  6268  frecxp  6314  fnfrec  6320