Theorem pm5.32da 439

Description: Distribution of implication over biconditional (deduction rule). (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 437	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  2363  reubida  2535  rmobida  2540  mpteq12f  3858  reuhypd  4221  funbrfv2b  5239  dffn5im  5240  eqfnfv2  5287  fndmin  5295  fniniseg  5308  rexsupp  5312  fmptco  5351  dff13  5428  riotabidva  5504  mpt2eq123dva  5586  mpt2eq3dva  5589  mpt2xopovel  5879  qliftfun  6211  erovlem  6221  xpcomco  6323  ltexpi  6527  dfplpq2  6544  axprecex  7046  zrevaddcl  8401  qrevaddcl  8729  icoshft  9012  fznn  9106  shftdm  9710  2shfti  9719  gcdaddm  10375