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  4748  opeqsng  5488  dfres3  5985  cores  6252  isoini  7338  eqfunresadj  7360  mpoeq123  7484  ordpwsuc  7812  xpord3pred  8149  rdglim2  8420  indpi1  12233  fzind  12695  btwnz  12700  elfzm11  13625  isprm2  16741  isprm3  16742  modprminv  16860  modprminveq  16861  isrngim2  20536  elimifd  32867  xrecex  33217  ordtconnlem1  34292  dfrdg4  36421  ee7.2aOLD  36950  expdioph  43730  cantnf2  44032  pm14.122b  45113  rexbidar  45135