Theorem pm5.32d 585

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 581	. 2 ⊢ ((𝜓 → (𝜒 ↔ 𝜃)) ↔ ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))
3	1, 2	sylib 220	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  pm5.32rd  586  pm5.32da  587  anbi2d  639  raltpd  4739  opeqsng  5471  dfres3  5968  cores  6232  isoini  7318  eqfunresadj  7340  mpoeq123  7464  ordpwsuc  7791  xpord3pred  8127  rdglim2  8398  indpi1  12206  fzind  12668  btwnz  12673  elfzm11  13597  isprm2  16699  isprm3  16700  modprminv  16818  modprminveq  16819  isrngim2  20481  elimifd  32691  xrecex  33058  ordtconnlem1  34182  dfrdg4  36265  ee7.2aOLD  36785  expdioph  43564  cantnf2  43866  pm14.122b  44963  rexbidar  44985