Theorem pm5.32da 440

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 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  2368  reubida  2540  rmobida  2545  mpteq12f  3878  reuhypd  4249  funbrfv2b  5271  dffn5im  5272  eqfnfv2  5319  fndmin  5327  fniniseg  5340  rexsupp  5344  fmptco  5383  dff13  5460  riotabidva  5536  mpt2eq123dva  5618  mpt2eq3dva  5621  mpt2xopovel  5911  qliftfun  6276  erovlem  6286  xpcomco  6392  ltexpi  6659  dfplpq2  6676  axprecex  7178  zrevaddcl  8552  qrevaddcl  8880  icoshft  9158  fznn  9252  shftdm  9929  2shfti  9938  sumeq2d  10415  sumeq2  10416  gcdaddm  10600