Theorem pm5.32da 433

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

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

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

This theorem depends on definitions:  df-bi 114

This theorem is referenced by:  rexbida  2338  reubida  2508  rmobida  2513  mpteq12f  3864  reuhypd  4230  funbrfv2b  5245  dffn5im  5246  eqfnfv2  5293  fndmin  5301  fniniseg  5314  rexsupp  5318  fmptco  5357  dff13  5434  riotabidva  5511  mpt2eq123dva  5593  mpt2eq3dva  5596  mpt2xopovel  5886  qliftfun  6218  erovlem  6228  xpcomco  6330  ltexpi  6492  dfplpq2  6509  axprecex  7011  zrevaddcl  8351  qrevaddcl  8675  icoshft  8958  fznn  9052  shftdm  9650  2shfti  9659