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  2315  reubida  2485  rmobida  2490  mpteq12f  3828  reuhypd  4169  funbrfv2b  5161  dffn5im  5162  eqfnfv2  5209  fndmin  5217  fniniseg  5230  rexsupp  5234  fmptco  5273  dff13  5350  riotabidva  5427  mpt2eq123dva  5508  mpt2eq3dva  5511  mpt2xopovel  5797  qliftfun  6124  erovlem  6134  xpcomco  6236  ltexpi  6321  dfplpq2  6338  axprecex  6764  zrevaddcl  8071  qrevaddcl  8353  icoshft  8628  fznn  8721