Theorem pm5.32d 670

Description: Distribution of implication over biconditional (deduction rule). (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 667	. 2 ⊢ ((𝜓 → (𝜒 ↔ 𝜃)) ↔ ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))
3	1, 2	sylib 208	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  pm5.32rd  671  pm5.32da  672  anbi2d  739  raltpd  4285  cores  5597  isoini  6542  mpt2eq123  6667  ordpwsuc  6962  rdglim2  7473  fzind  11419  btwnz  11423  elfzm11  12352  isprm2  15319  isprm3  15320  modprminv  15428  modprminveq  15429  isrim  18654  elimifd  29206  funcnvmptOLD  29307  xrecex  29410  ordtconnlem1  29749  indpi1  29862  dfres3  31354  dfrdg4  31697  ee7.2aOLD  32099  wl-ax11-lem8  32998  expdioph  37067  pm14.122b  38103  rexbidar  38129  mapsnend  38862  isrngim  41189