Theorem pm5.32da 425

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 108	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))
3	2	pm5.32d 423	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  rexbida  2321  reubida  2491  rmobida  2496  mpteq12f  3837  reuhypd  4203  funbrfv2b  5218  dffn5im  5219  eqfnfv2  5266  fndmin  5274  fniniseg  5287  rexsupp  5291  fmptco  5330  dff13  5407  riotabidva  5484  mpt2eq123dva  5566  mpt2eq3dva  5569  mpt2xopovel  5856  qliftfun  6188  erovlem  6198  xpcomco  6300  ltexpi  6435  dfplpq2  6452  axprecex  6954  zrevaddcl  8295  qrevaddcl  8578  icoshft  8858  fznn  8951  shftdm  9423  2shfti  9432