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

Assertion

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

Proof of Theorem anbi1d

Step	Hyp	Ref	Expression
1		bid.1	. . 3 ⊢ (φ → (ψ ↔ χ))
2	1	a1d 22	. 2 ⊢ (φ → (θ → (ψ ↔ χ)))
3	2	pm5.32rd 621	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:  anbi1  687  anbi12d  691  bi2anan9  843  pm5.71  902  cador  1391  drsb1  2022  eleq1  2413  rexeqf  2805  reueq1f  2806  rmoeq1f  2807  rabeqf  2853  vtocl2gaf  2922  alexeq  2969  ceqex  2970  sbc2or  3055  sbc5  3071  rexss  3334  psstr  3374  ineq1  3451  difin2  3517  r19.28z  3643  r19.28zv  3646  ssunsn2  3866  eluni  3895  pwadjoin  4120  preq12bg  4129  elxpk  4197  opkelopkabg  4246  opkelxpkg  4248  otkelins2kg  4254  otkelins3kg  4255  opkelcokg  4262  opkelimagekg  4272  insklem  4305  ssfin  4471  ncfinraise  4482  evenodddisj  4517  nnpweq  4524  sfineq1  4527  vfinspss  4552  copsexg  4608  elopab  4697  setconslem6  4737  xpeq1  4799  elxpi  4801  vtoclr  4817  opbrop  4842  brswap2  4861  brco  4884  resopab2  5002  elxp4  5109  fun11  5160  feq2  5212  f1eq2  5255  f1eq3  5256  foeq2  5267  tz6.12-2  5347  dmfco  5382  respreima  5411  isoeq5  5487  isomin  5497  isoini  5498  f1oiso  5500  f1oiso2  5501  brswap  5510  oprabid  5551  dfoprab2  5559  eloprabga  5579  resoprab  5582  resoprab2  5583  ov  5596  ov3  5600  ov6g  5601  ovg  5602  mpteq12f  5656  mpt2eq123  5662  trtxp  5782  oqelins4  5795  txpcofun  5804  qrpprod  5837  dmpprod  5841  clos1eq1  5875  trd  5922  frd  5923  elpmg  6014  lecex  6116  ncspw1eu  6160  leltctr  6213  ce2le  6234  nmembers1lem1  6269  frecxp  6315  fnfrec  6321