Theorem pm5.32d 587

Description: Distribution of implication over biconditional (deduction form). (Contributed by NM, 29-Oct-1996.)

Hypothesis

Ref	Expression
pm5.32d.1	⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))

Assertion

Ref	Expression
pm5.32d	⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))

Proof of Theorem pm5.32d

Step	Hyp	Ref	Expression
1		pm5.32d.1	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))
2		pm5.32 583	. 2 ⊢ ((𝜓 → (𝜒 ↔ 𝜃)) ↔ ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))
3	1, 2	sylib 221	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 401

This theorem is referenced by:  pm5.32rd  588  pm5.32da  589  anbi2d  641  raltpd  4743  opeqsng  5477  dfres3  5974  cores  6240  isoini  7326  eqfunresadj  7348  mpoeq123  7472  ordpwsuc  7799  xpord3pred  8136  rdglim2  8407  indpi1  12223  fzind  12685  btwnz  12690  elfzm11  13614  isprm2  16730  isprm3  16731  modprminv  16849  modprminveq  16850  isrngim2  20526  elimifd  32799  xrecex  33152  ordtconnlem1  34231  dfrdg4  36314  ee7.2aOLD  36834  expdioph  43612  cantnf2  43914  pm14.122b  44997  rexbidar  45019