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  4752  opeqsng  5487  dfres3  5984  cores  6251  isoini  7337  eqfunresadj  7359  mpoeq123  7483  ordpwsuc  7811  xpord3pred  8148  rdglim2  8419  indpi1  12232  fzind  12694  btwnz  12699  elfzm11  13623  isprm2  16740  isprm3  16741  modprminv  16859  modprminveq  16860  isrngim2  20535  elimifd  32830  xrecex  33180  ordtconnlem1  34259  dfrdg4  36376  ee7.2aOLD  36895  expdioph  43676  cantnf2  43978  pm14.122b  45059  rexbidar  45081