Theorem pm5.32da 440

Description: Distribution of implication over biconditional (deduction form). (Contributed by NM, 9-Dec-2006.)

Hypothesis

Ref	Expression
pm5.32da.1	⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))

Assertion

Ref	Expression
pm5.32da	⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))

Proof of Theorem pm5.32da

Step	Hyp	Ref	Expression
1		pm5.32da.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))
2	1	ex 113	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))
3	2	pm5.32d 438	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 102   ↔ wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  rexbida  2375  reubida  2548  rmobida  2553  mpteq12f  3918  reuhypd  4293  funbrfv2b  5349  dffn5im  5350  eqfnfv2  5398  fndmin  5406  fniniseg  5419  rexsupp  5423  fmptco  5464  dff13  5547  riotabidva  5624  mpt2eq123dva  5710  mpt2eq3dva  5713  mpt2xopovel  6006  qliftfun  6372  erovlem  6382  xpcomco  6540  ltexpi  6894  dfplpq2  6911  axprecex  7413  zrevaddcl  8798  qrevaddcl  9127  icoshft  9405  fznn  9499  shftdm  10252  2shfti  10261  sumeq2  10744  fisum  10774  fsum2dlemstep  10824  gcdaddm  11249  elcncf2  11585